diff --git a/250929-colloquium.pdf b/250929-colloquium.pdf new file mode 100644 index 0000000..b28c481 Binary files /dev/null and b/250929-colloquium.pdf differ diff --git a/250929-colloquium.potx b/250929-colloquium.potx index d1102cb..915099f 100644 Binary files a/250929-colloquium.potx and b/250929-colloquium.potx differ diff --git a/ColloquiumLean/ContinuousLimit.lean b/ColloquiumLean/ContinuousLimit.lean index fccfbb5..149c3f4 100644 --- a/ColloquiumLean/ContinuousLimit.lean +++ b/ColloquiumLean/ContinuousLimit.lean @@ -1,5 +1,5 @@ +-- Library Import: Basic facts about real numbers import Mathlib - open Real -- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ) @@ -15,8 +15,10 @@ def seq_limit (u : ℕ → ℝ) (l : ℝ) := variable {f : ℝ → ℝ} {u : ℕ → ℝ} {x₀ : ℝ} - -lemma continuity_and_limits - (hyp_f : continuous_at f x₀) (hyp_u : seq_limit u x₀) : +/- +Theorem "Continuity and Limits": If the function f is continuous at x₀ and u +is a sequence converging to x₀, then the sequence f ∘ u converges to f (x₀). +-/ +theorem continuity_and_limits (hyp_f : continuous_at f x₀) (hyp_u : seq_limit u x₀) : seq_limit (f ∘ u) (f x₀) := by sorry diff --git a/ColloquiumLean/ContinuousSquare.lean b/ColloquiumLean/ContinuousSquare.lean deleted file mode 100644 index 1c8d1b1..0000000 --- a/ColloquiumLean/ContinuousSquare.lean +++ /dev/null @@ -1,35 +0,0 @@ -import Mathlib - -open Real - -variable - {x : ℝ} {y : ℝ} - --- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ) -def continuous_at (f : ℝ → ℝ) (x₀ : ℝ) := - ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε - --- Three lemmas from the lean mathematical library -example : 0 < x → 0 < √x := sqrt_pos.2 - -example : x ^ 2 < y ↔ (-√y < x) ∧ (x < √y) := sq_lt - -example : |x| < y ↔ -y < x ∧ x < y := abs_lt - --- The square function -def squareFct : ℝ → ℝ := fun x ↦ x ^ 2 - - -theorem continuous_at_squareFct : - continuous_at squareFct 0 := by - unfold continuous_at - intro e he - use √e - constructor - · apply sqrt_pos.2 - exact he - · intro x hx - simp_all [squareFct] - apply sq_lt.2 - apply abs_lt.1 - exact hx diff --git a/ColloquiumLean/ContinuousSquareSolution.lean b/ColloquiumLean/ContinuousSquareSolution.lean deleted file mode 100644 index 3f6ad00..0000000 --- a/ColloquiumLean/ContinuousSquareSolution.lean +++ /dev/null @@ -1,39 +0,0 @@ --- Library Import: Basic facts about real numbers and the root function -import Mathlib.Data.Real.Sqrt -open Real - --- In the following, x and y are real numbers -variable {x : ℝ} {y : ℝ} - --- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ) -def continuous (f : ℝ → ℝ) (x₀ : ℝ) := - ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε - --- Definition: The square function -def squareFct : ℝ → ℝ := fun x ↦ x ^ 2 - - --- Reminder: Three facts from the library that we will use. -example : 0 < x → 0 < √x := sqrt_pos.2 - -example : x ^ 2 < y ↔ (-√y < x) ∧ (x < √y) := sq_lt - -example : |x| < y ↔ -y < x ∧ x < y := abs_lt - - --- Theorem: The square function is continuous at x₀ = 0 -theorem ContinuousAt_sq : - continuous squareFct 0 := by - - unfold continuous - - intro ε hε - use √ε - - constructor - · apply sqrt_pos.2 - exact hε - · intro x hx - simp_all [squareFct] - apply sq_lt.2 - exact abs_lt.1 hx diff --git a/ColloquiumLean/Jensen.lean b/ColloquiumLean/Jensen.lean new file mode 100644 index 0000000..499baf4 --- /dev/null +++ b/ColloquiumLean/Jensen.lean @@ -0,0 +1,181 @@ +/- +Copyright (c) 2025 Stefan Kebekus. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Stefan Kebekus +-/ +import Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction +import ColloquiumLean.PosLogEqCircleAverage + +/-! +# Jensen's Formula of Complex Analysis + +If a function `g : ℂ → ℂ` is analytic without zero on the closed ball with +center `c` and radius `R`, then `log ‖g ·‖` is harmonic, and the mean value +theorem of harmonic functions asserts that the circle average `circleAverage +(log ‖g ·‖) c R` equals `log ‖g c‖`. Note that `g c` equals +`meromorphicTrailingCoeffAt f c` and see `circleAverage_nonVanishAnalytic` for +the precise statement. + +Jensen's Formula generalizes this to the setting where `g` is merely +meromorphic. In that case, the `circleAverage (log ‖g ·‖) 0 R` equals `log +`‖meromorphicTrailingCoeffAt g 0‖` plus a correction term that accounts for the +zeros of poles of `g` within the ball. +-/ + +open Filter MeromorphicAt MeromorphicOn Metric Real + +variable + {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] + +-- Should go to Mathlib.Analysis.Complex.ValueDistribution.CountingFunction +lemma Function.locallyFinsuppWithin.countingFunction_finsum_eq_finsum_add' {c : ℂ} {R : ℝ} + {D : ℂ → ℤ} (hR : R ≠ 0) (hD : D.support.Finite) : + ∑ᶠ u, D u * (log R - log ‖c - u‖) = ∑ᶠ u, D u * log (R * ‖c - u‖⁻¹) + D c * log R := by + by_cases h : c ∈ D.support + · have {g : ℂ → ℝ} : (fun u ↦ D u * g u).support ⊆ hD.toFinset := + fun x ↦ by simp +contextual + simp only [finsum_eq_sum_of_support_subset _ this, + Finset.sum_eq_sum_diff_singleton_add ((Set.Finite.mem_toFinset hD).mpr h), sub_self, + norm_zero, log_zero, sub_zero, inv_zero, mul_zero, add_zero, add_left_inj] + refine Finset.sum_congr rfl fun x hx ↦ ?_ + simp only [Finset.mem_sdiff, Finset.notMem_singleton] at hx + rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 hx.2.symm))), log_inv] + ring + · simp_all only [mem_support, Decidable.not_not, Int.cast_zero, zero_mul, add_zero] + refine finsum_congr fun x ↦ ?_ + by_cases h₁ : c = x + · simp_all + · rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv] + ring + +/-! +## Circle Averages + +In preparation to the proof of Jensen's formula, compute several circle +averages. +-/ + +/-- +Let `D : ℂ → ℤ` be a function with locally finite support within the closed ball +with center `c` and radius `R`, such as the zero- and pole divisor of a +meromorphic function. Then, the circle average of the associated factorized +rational function over the boundary of the ball equals `∑ᶠ u, (D u) * log R`. +-/ +@[simp] +lemma circleAverage_logAbs_factorizedRational {R : ℝ} {c : ℂ} + (D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ) : + circleAverage (∑ᶠ u, ((D u) * log ‖· - u‖)) c R = ∑ᶠ u, (D u) * log R := by + have h := D.finiteSupport (isCompact_closedBall c |R|) + calc circleAverage (∑ᶠ u, ((D u) * log ‖· - u‖)) c R + _ = circleAverage (∑ u ∈ h.toFinset, ((D u) * log ‖· - u‖)) c R := by + rw [finsum_eq_sum_of_support_subset] + intro u + contrapose + aesop + _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ ↑(D i) * log ‖x - i‖) c R := by + rw [circleAverage_sum] + intro u hu + apply IntervalIntegrable.const_mul + apply circleIntegrable_log_norm_meromorphicOn (f := (· - u)) + apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn + _ = ∑ u ∈ h.toFinset, ↑(D u) * log R := by + apply Finset.sum_congr rfl + intro u hu + simp_rw [← smul_eq_mul, circleAverage_fun_smul] + congr + apply circleAverage_logAbs_affine + apply D.supportWithinDomain + simp_all + _ = ∑ᶠ u, (D u) * log R := by + rw [finsum_eq_sum_of_support_subset] + intro u + aesop + +/-- +If `g : ℂ → ℂ` is analytic without zero on the closed ball with center `c` and +radius `R`, then the circle average `circleAverage (log ‖g ·‖) c R` equals `log +‖g c‖`. +-/ +@[simp] +lemma circleAverage_nonVanishAnalytic {R : ℝ} {c : ℂ} {g : ℂ → ℂ} + (h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)) + (h₂g : ∀ u : closedBall c |R|, g u ≠ 0) : + circleAverage (log ‖g ·‖) c R = log ‖g c‖ := + HarmonicOnNhd.circleAverage_eq (fun x hx ↦ (h₁g x hx).harmonicAt_log_norm (h₂g ⟨x, hx⟩)) + +/-! +## Jensen's Formula +-/ + +/-! +**Jensen's Formula**: If `f : ℂ → ℂ` is meromorphic on the closed ball with +center `c` and radius `R`, then the `circleAverage (log ‖f ·‖) 0 R` equals `log +`‖meromorphicTrailingCoeffAt f 0‖` plus a correction term that accounts for the +zeros of poles of `f` within the ball. +-/ +theorem MeromorphicOn.JensenFormula {c : ℂ} {R : ℝ} {f : ℂ → ℂ} (hR : R ≠ 0) + (h₁f : MeromorphicOn f (closedBall c |R|)) : + circleAverage (log ‖f ·‖) c R + = ∑ᶠ u, divisor f (closedBall c |R|) u * log (R * ‖c - u‖⁻¹) + + divisor f (closedBall c |R|) c * log R + log ‖meromorphicTrailingCoeffAt f c‖ := by + -- Shorthand notation to keep line size in check + let CB := closedBall c |R| + by_cases h₂f : ∀ u : CB, meromorphicOrderAt f u ≠ ⊤ + · have h₃f := (divisor f CB).finiteSupport (isCompact_closedBall c |R|) + -- Extract zeros & poles and compute + obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₁f.extract_zeros_poles h₂f h₃f + calc circleAverage (log ‖f ·‖) c R + _ = circleAverage ((∑ᶠ u, (divisor f CB u * log ‖· - u‖)) + (log ‖g ·‖)) c R := by + have h₄g := extract_zeros_poles_log h₂g h₃g + rw [circleAverage_congr_codiscreteWithin (codiscreteWithin.mono sphere_subset_closedBall h₄g) + hR] + _ = circleAverage (∑ᶠ u, (divisor f CB u * log ‖· - u‖)) c R + circleAverage (log ‖g ·‖) c R + := by + apply circleAverage_add + · exact circleIntegrable_log_norm_factorizedRational (divisor f CB) + · exact circleIntegrable_log_norm_meromorphicOn + (h₁g.mono sphere_subset_closedBall).meromorphicOn + _ = ∑ᶠ u, divisor f CB u * log R + log ‖g c‖ := by simp [h₁g, h₂g] + _ = ∑ᶠ u, divisor f CB u * log R + + (log ‖meromorphicTrailingCoeffAt f c‖ - ∑ᶠ u, divisor f CB u * log ‖c - u‖) := by + have t₀ : c ∈ CB := by simp [CB] + have t₁ : AccPt c (𝓟 CB) := by + apply accPt_iff_frequently_nhdsNE.mpr + apply compl_notMem + apply mem_nhdsWithin.mpr + use ball c |R| + simpa [hR] using fun _ ⟨h, _⟩ ↦ ball_subset_closedBall h + simp [MeromorphicOn.log_norm_meromorphicTrailingCoeffAt_extract_zeros_poles + h₃f t₀ t₁ (h₁f c t₀) (h₁g c t₀) (h₂g ⟨c, t₀⟩) h₃g] + _ = ∑ᶠ u, divisor f CB u * log R - ∑ᶠ u, divisor f CB u * log ‖c - u‖ + + log ‖meromorphicTrailingCoeffAt f c‖ := by + ring + _ = (∑ᶠ u, divisor f CB u * (log R - log ‖c - u‖)) + log ‖meromorphicTrailingCoeffAt f c‖ := by + rw [← finsum_sub_distrib] + · simp_rw [← mul_sub] + · apply h₃f.subset (fun _ ↦ (by simp_all)) + · apply h₃f.subset (fun _ ↦ (by simp_all)) + _ = ∑ᶠ u, divisor f CB u * log (R * ‖c - u‖⁻¹) + divisor f CB c * log R + + log ‖meromorphicTrailingCoeffAt f c‖ := by + rw [Function.locallyFinsuppWithin.countingFunction_finsum_eq_finsum_add' hR h₃f] + · -- Trivial case: `f` vanishes on a codiscrete set + rw [← h₁f.exists_meromorphicOrderAt_ne_top_iff_forall + ⟨nonempty_closedBall.mpr (abs_nonneg R), (convex_closedBall c |R|).isPreconnected⟩] at h₂f + push_neg at h₂f + have : divisor f CB = 0 := by + ext x + by_cases h : x ∈ CB + <;> simp_all [CB] + simp only [CB, this, Function.locallyFinsuppWithin.coe_zero, Pi.zero_apply, Int.cast_zero, + zero_mul, finsum_zero, add_zero, zero_add] + rw [MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top (by aesop), norm_zero, log_zero] + have : f =ᶠ[codiscreteWithin CB] 0 := by + filter_upwards [h₁f.meromorphicNFAt_mem_codiscreteWithin, self_mem_codiscreteWithin CB] + with z h₁z h₂z + simpa [h₂f ⟨z, h₂z⟩] using (not_iff_not.2 h₁z.meromorphicOrderAt_eq_zero_iff) + rw [circleAverage_congr_codiscreteWithin (f₂ := 0) _ hR] + · simp only [circleAverage, mul_inv_rev, Pi.zero_apply, intervalIntegral.integral_zero, + smul_eq_mul, mul_zero] + apply Filter.codiscreteWithin.mono (U := CB) sphere_subset_closedBall + filter_upwards [this] with z hz + simp_all diff --git a/ColloquiumLean/PosLogEqCircleAverage.lean b/ColloquiumLean/PosLogEqCircleAverage.lean new file mode 100644 index 0000000..99f1008 --- /dev/null +++ b/ColloquiumLean/PosLogEqCircleAverage.lean @@ -0,0 +1,269 @@ +/- +Copyright (c) 2025 Stefan Kebekus. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Stefan Kebekus +-/ +import Mathlib.Analysis.Complex.Harmonic.MeanValue +import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions +import Mathlib.Analysis.SpecialFunctions.Integrals.Basic +import Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric +import Mathlib.MeasureTheory.Integral.CircleAverage + +/-! +# Representation of `log⁺` as a Circle Average + +If `a` is any complex number, the circle average of `log ‖· - a‖` over the unit +circle equals the positive part of the logarithm, +`circleAverage (log ‖· - a‖) 0 1 = log⁺ ‖a‖`. +-/ + +open Filter Interval intervalIntegral MeasureTheory Metric Real + +variable {a c : ℂ} {R : ℝ} + +/-! +## Circle Integrability +-/ + +/-- +If `a` is any complex number, the function `(log ‖· - a‖)` is circle integrable over every circle. +-/ +lemma circleIntegrable_log_norm_sub_const (r : ℝ) : + CircleIntegrable (log ‖· - a‖) c r := + circleIntegrable_log_norm_meromorphicOn (fun z hz ↦ by fun_prop) + +/-! +## Computing `circleAverage (log ‖· - a‖) 0 1` in case where `‖a‖ < 1`. +-/ + +/-- +If `a : ℂ` has norm smaller than one, then `circleAverage (log ‖· - a‖) 0 1` +vanishes. +-/ +@[simp] +theorem circleAverage_log_norm_sub_const₀ (h : ‖a‖ < 1) : + circleAverage (log ‖· - a‖) 0 1 = 0 := by + calc circleAverage (log ‖· - a‖) 0 1 + _ = circleAverage (log ‖1 - ·⁻¹ * a‖) 0 1 := by + apply circleAverage_congr_sphere + intro z hz + simp_all only [abs_one, mem_sphere_iff_norm, sub_zero] + congr 1 + calc ‖z - a‖ + _ = 1 * ‖z - a‖ := + (one_mul ‖z - a‖).symm + _ = ‖z⁻¹‖ * ‖z - a‖ := by + simp_all + _ = ‖z⁻¹ * (z - a)‖ := + (Complex.norm_mul z⁻¹ (z - a)).symm + _ = ‖z⁻¹ * z - z⁻¹ * a‖ := by + rw [mul_sub] + _ = ‖1 - z⁻¹ * a‖ := by + rw [inv_mul_cancel₀] + aesop + _ = 0 := by + rw [circleAverage_zero_one_congr_inv (f := fun x ↦ log ‖1 - x * a‖), + HarmonicOnNhd.circleAverage_eq, + zero_mul, sub_zero, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, log_one] + intro x hx + have : ‖x * a‖ < 1 := by + calc ‖x * a‖ + _ = ‖x‖ * ‖a‖ := by simp + _ ≤ ‖a‖ := by + by_cases ‖a‖ = 0 + <;> aesop + _ < 1 := h + apply AnalyticAt.harmonicAt_log_norm (by fun_prop) + rw [sub_ne_zero] + by_contra! hCon + rwa [← hCon, CStarRing.norm_of_mem_unitary (unitary ℂ).one_mem, lt_self_iff_false] at this + +/-! +## Computing `circleAverage (log ‖· - a‖) 0 1` in case where `‖a‖ = 1`. +-/ + +-- Integral computation used in `circleAverage_log_norm_id_sub_const₁` +private lemma circleAverage_log_norm_sub_const₁_integral : + ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 = 0 := by + calc ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 + _ = ∫ (x : ℝ) in 0..π, log (4 * sin x ^ 2) := by + have {x : ℝ} : x / 2 = 2⁻¹ * x := by ring + rw [intervalIntegral.integral_div, this, inv_mul_integral_comp_div + (f := fun x ↦ log (4 * sin x ^ 2))] + simp + _ = ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) := by + apply integral_congr_codiscreteWithin + apply codiscreteWithin.mono (by tauto : Ι 0 π ⊆ Set.univ) + have : AnalyticOnNhd ℝ (4 * sin · ^ 2) Set.univ := fun _ _ ↦ by fun_prop + have := this.preimage_zero_mem_codiscrete (x := π / 2) + simp only [sin_pi_div_two, one_pow, mul_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, + Set.preimage_compl, forall_const] at this + filter_upwards [this] with a ha + simp only [Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff, mul_eq_zero, + OfNat.ofNat_ne_zero, ne_eq, not_false_eq_true, pow_eq_zero_iff, false_or] at ha + rw [log_mul (by norm_num) (by simp_all), log_pow, Nat.cast_ofNat] + _ = (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) := by + rw [integral_add _root_.intervalIntegrable_const + (by apply intervalIntegrable_log_sin.const_mul 2), intervalIntegral.integral_const_mul] + _ = 0 := by + simp only [intervalIntegral.integral_const, sub_zero, smul_eq_mul, integral_log_sin_zero_pi, + (by norm_num : (4 : ℝ) = 2 * 2), log_mul two_ne_zero two_ne_zero] + ring + +/-- +If `a : ℂ` has norm one, then the circle average `circleAverage (log ‖· - a‖) 0 1` vanishes. +-/ +@[simp] +theorem circleAverage_log_norm_sub_const₁ (h : ‖a‖ = 1) : + circleAverage (log ‖· - a‖) 0 1 = 0 := by + -- Observing that the problem is rotation invariant, we rotate by an angle of `ζ = - arg a` and + -- reduce the problem to the case where `a = 1`. The integral can then be evalutated by a direct + -- computation. + simp only [circleAverage, mul_inv_rev, smul_eq_mul, mul_eq_zero, inv_eq_zero, OfNat.ofNat_ne_zero, + or_false] + right + obtain ⟨ζ, hζ⟩ : ∃ ζ, a⁻¹ = circleMap 0 1 ζ := by simp [Set.exists_range_iff.1, h] + calc ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - a‖ + _ = ∫ x in 0..(2 * π), log ‖(circleMap 0 1 ζ) * (circleMap 0 1 x - a)‖ := by + simp + _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - (circleMap 0 1 ζ) * a‖ := by + simp [mul_sub, circleMap, add_mul, Complex.exp_add] + _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 (ζ + x) - 1‖ := by + simp [← hζ, inv_mul_cancel₀ (by aesop : a ≠ 0)] + _ = ∫ x in 0..(2 * π), log ‖circleMap 0 1 x - 1‖ := by + have : Function.Periodic (log ‖circleMap 0 1 · - 1‖) (2 * π) := + fun x ↦ by simp [periodic_circleMap 0 1 x] + have := this.intervalIntegral_add_eq (t := 0) (s := ζ) + simp_all [integral_comp_add_left (log ‖circleMap 0 1 · - 1‖)] + _ = ∫ x in 0..(2 * π), log (4 * sin (x / 2) ^ 2) / 2 := by + apply integral_congr + intro x hx + simp only [] + rw [Complex.norm_def, log_sqrt (circleMap 0 1 x - 1).normSq_nonneg] + congr + calc Complex.normSq (circleMap 0 1 x - 1) + _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by + simp [circleMap, Complex.normSq_apply] + _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by + ring + _ = 2 - 2 * cos x := by + rw [sin_sq_add_cos_sq] + norm_num + _ = 2 - 2 * cos (2 * (x / 2)) := by + rw [← mul_div_assoc] + norm_num + _ = 4 - 4 * cos (x / 2) ^ 2 := by + rw [cos_two_mul] + ring + _ = 4 * sin (x / 2) ^ 2 := by + nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)] + ring + _ = 0 := circleAverage_log_norm_sub_const₁_integral + +/-! +## Computing `circleAverage (log ‖· - a‖) 0 1` in case where `1 < ‖a‖`. +-/ + +/-- +If `a : ℂ` has norm greater than one, then `circleAverage (log ‖· - a‖) 0 1` +equals `log ‖a‖`. +-/ +@[simp] +theorem circleAverage_log_norm_sub_const₂ (h : 1 < ‖a‖) : + circleAverage (log ‖· - a‖) 0 1 = log ‖a‖ := by + rw [HarmonicOnNhd.circleAverage_eq, zero_sub, norm_neg] + intro x hx + apply AnalyticAt.harmonicAt_log_norm (by fun_prop) + rw [sub_ne_zero] + by_contra! + simp_all only [abs_one, Metric.mem_closedBall, dist_zero_right] + linarith + +/-! +## Presentation of `log⁺` in Terms of Circle Averages +-/ + +/-- +The `circleAverage (log ‖· - a‖) 0 1` equals `log⁺ ‖a‖`. +-/ +@[simp] +theorem circleAverage_log_norm_sub_const_eq_posLog : + circleAverage (log ‖· - a‖) 0 1 = log⁺ ‖a‖ := by + rcases lt_trichotomy 1 ‖a‖ with h | h | h + · rw [circleAverage_log_norm_sub_const₂ h] + apply (posLog_eq_log _).symm + simp_all [le_of_lt h] + · rw [eq_comm, circleAverage_log_norm_sub_const₁ h.symm, posLog_eq_zero_iff] + simp_all + · rw [eq_comm, circleAverage_log_norm_sub_const₀ h, posLog_eq_zero_iff] + simp_all [le_of_lt h] + +/-- +The `circleAverage (log ‖· + a‖) 0 1` equals `log⁺ ‖a‖`. +-/ +@[simp] +theorem circleAverage_log_norm_add_const_eq_posLog : + circleAverage (log ‖· + a‖) 0 1 = log⁺ ‖a‖ := by + have : (log ‖· + a‖) = (log ‖· - -a‖) := by simp + simp [this] + +/-- +Generalization of `circleAverage_log_norm_sub_const_eq_posLog`: The +`circleAverage (log ‖· - a‖) c R` equals `log R + log⁺ (|R|⁻¹ * ‖c - a‖)`. +-/ +theorem circleAverage_log_norm_sub_const_eq_log_radius_add_posLog (hR : R ≠ 0) : + circleAverage (log ‖· - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖) := by + calc circleAverage (log ‖· - a‖) c R + _ = circleAverage (fun z ↦ log ‖R * (z + R⁻¹ * (c - a))‖) 0 1 := by + rw [circleAverage_eq_circleAverage_zero_one] + congr + ext z + congr + rw [Complex.ofReal_inv R] + field_simp [Complex.ofReal_ne_zero.mpr hR] + ring + _ = circleAverage (fun z ↦ log ‖R‖ + log ‖z + R⁻¹ * (c - a)‖) 0 1 := by + apply circleAverage_congr_codiscreteWithin _ (zero_ne_one' ℝ).symm + have : {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (Metric.sphere (0 : ℂ) |1|) := by + apply codiscreteWithin_iff_locallyFiniteComplementWithin.2 + intro z hz + use Set.univ + simp only [univ_mem, abs_one, Complex.ofReal_inv, ne_eq, norm_eq_zero, Set.univ_inter, + true_and] + apply Set.Subsingleton.finite + intro z₁ hz₁ z₂ hz₂ + simp_all only [ne_eq, abs_one, mem_sphere_iff_norm, sub_zero, Set.mem_diff, Set.mem_setOf_eq, + Decidable.not_not] + rw [add_eq_zero_iff_eq_neg.1 hz₁.2, add_eq_zero_iff_eq_neg.1 hz₂.2] + filter_upwards [this] with z hz + rw [norm_mul, log_mul (norm_ne_zero_iff.2 (Complex.ofReal_ne_zero.mpr hR)) hz] + simp + _ = log R + log⁺ (|R|⁻¹ * ‖c - a‖) := by + have : (fun z ↦ log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖) = + (fun z ↦ log ‖R‖) + (fun z ↦ log ‖z + ↑R⁻¹ * (c - a)‖) := by + rfl + rw [this, circleAverage_add (circleIntegrable_const (log ‖R‖) 0 1) + (circleIntegrable_log_norm_meromorphicOn (fun _ _ ↦ by fun_prop)), circleAverage_const] + simp + _ = log R + log⁺ (R⁻¹ * ‖c - a‖) := by + congr 1 + rcases lt_trichotomy 0 R with h | h | h + · rw [abs_of_pos h] + · tauto + · simp [abs_of_neg h] + +/-- +Trivial corollary of +`circleAverage_log_norm_sub_const_eq_log_radius_add_posLog`: If `u : ℂ` lies +within the closed ball with center `c` and radius `R`, then the circle average +`circleAverage (log ‖· - u‖) c R` equals `log R`. +-/ +@[simp] +lemma circleAverage_logAbs_affine (hu : a ∈ closedBall c |R|) : + circleAverage (log ‖· - a‖) c R = log R := by + by_cases hR : R = 0 + · simp_all + rw [circleAverage_log_norm_sub_const_eq_log_radius_add_posLog hR, add_eq_left, + posLog_eq_zero_iff, abs_mul, abs_inv, abs_of_nonneg (norm_nonneg (c - a))] + rw [mem_closedBall, dist_eq_norm'] at hu + apply inv_mul_le_one_of_le₀ hu (abs_nonneg R) diff --git a/lake-manifest.json b/lake-manifest.json index 597776a..0ab921c 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e2a81062ed182504d3c853c09109e93b7916e97a", + "rev": "fed4c2fb23c918fc0263376a64404eb166aadd0f", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9", + "rev": "9f492660e9837df43fd885a2ad05c520da9ff9f5", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7fca1d4a190761bac0028848f73dc9a59fcb4957", + "rev": "90f3b0f429411beeeb29bbc248d799c18a2d520d", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e47cc88cfbf1601ab364e9a4de5f33f13401ff8", + "rev": "556caed0eadb7901e068131d1be208dd907d07a2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.71", + "inputRev": "v0.0.74", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "247ff80701c76760523b5d7c180b27b7708faf38", + "rev": "9e8de5716b162ec8983a89711a186d13ff871c22", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9b703a545097978aef0e7e243ab8b71c32a9ff65", + "rev": "2e582a44b0150db152bff1c8484eb557fb5340da", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d117e2c28cba42e974bc22568ac999492a34e812", + "rev": "903b509acff8e83c0dd7820d164968e0cb941b97", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc", + "rev": "b62fd39acc32da6fb8bb160c82d1bbc3cb3c186e", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/lean-toolchain b/lean-toolchain index 7f254a9..66a6d41 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.23.0 +leanprover/lean4:v4.24.0-rc1 \ No newline at end of file