Compare commits

...

2 Commits

Author SHA1 Message Date
Stefan Kebekus a1f96806a1 Working… 2024-08-01 12:38:33 +02:00
Stefan Kebekus f65c84a14b working… 2024-08-01 10:02:36 +02:00
4 changed files with 494 additions and 20 deletions

View File

@ -1,6 +1,13 @@
import Nevanlinna.harmonicAt_examples
import Nevanlinna.harmonicAt_meanValue
lemma int₀
{a : }
(ha : a ∈ Metric.ball 0 1)
:
∫ (x : ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a‖ = 0 := by
sorry
theorem jensen_case_R_eq_one
(f : )
@ -64,21 +71,32 @@ theorem jensen_case_R_eq_one
exact hz A
have s₁ : ∀ z, f z ≠ 0 → logAbsF z = logAbsf z - ∑ s, Real.log ‖z - a s‖ := by
sorry
intro z hz
rw [s₀ z hz]
simp
rw [s₁ 0 h₂f] at t₁
have {x : } : f (circleMap 0 1 x) ≠ 0 := by
sorry
have h₀ {x : } : f (circleMap 0 1 x) ≠ 0 := by
rw [h₃F]
simp
constructor
· exact h₂F (circleMap 0 1 x)
· by_contra h'
obtain ⟨s, _, h₂s⟩ := Finset.prod_eq_zero_iff.1 h'
have : circleMap 0 1 x = a s := by
rw [← sub_zero (circleMap 0 1 x)]
nth_rw 2 [← h₂s]
simp
let A := ha s
rw [← this] at A
simp at A
simp_rw [s₁ (circleMap 0 1 _) this] at t₁
simp_rw [s₁ (circleMap 0 1 _) h₀] at t₁
rw [intervalIntegral.integral_sub] at t₁
rw [intervalIntegral.integral_finset_sum] at t₁
have {i : S} : ∫ (x : ) in (0)..2 * Real.pi, Real.log ‖circleMap 0 1 x - a i‖ = 0 := by
sorry
simp_rw [this] at t₁
simp_rw [int₀ (ha _)] at t₁
simp at t₁
rw [t₁]
simp
@ -89,7 +107,7 @@ theorem jensen_case_R_eq_one
simp
rfl
-- ∀ i ∈ Finset.univ, IntervalIntegrable (fun x => Real.log ‖circleMap 0 1 x - a i‖) MeasureTheory.volume 0 (2 * Real.pi)
intro i hi
intro i _
apply Continuous.intervalIntegrable
apply continuous_iff_continuousAt.2
intro x
@ -115,7 +133,7 @@ theorem jensen_case_R_eq_one
rw [this]
apply ContinuousAt.comp
simp
sorry
exact h₀
apply ContinuousAt.comp
apply Complex.continuous_abs.continuousAt
apply ContinuousAt.comp
@ -125,7 +143,7 @@ theorem jensen_case_R_eq_one
-- IntervalIntegrable (fun x => ∑ s : { x // x ∈ S }, Real.log ‖circleMap 0 1 x - a s‖) MeasureTheory.volume 0 (2 * Real.pi)
apply Continuous.intervalIntegrable
apply continuous_finset_sum
intro i hi
intro i _
apply continuous_iff_continuousAt.2
intro x
have : (fun x => Real.log ‖circleMap 0 1 x - a i‖) = Real.log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - a i) :=

View File

@ -0,0 +1,456 @@
import Mathlib.Analysis.Complex.TaylorSeries
noncomputable def primitive
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] :
→ ( → E) → ( → E) := by
intro z₀
intro f
exact fun z ↦ (∫ (x : ) in z₀.re..z.re, f ⟨x, z₀.im⟩) + Complex.I • ∫ (x : ) in z₀.im..z.im, f ⟨z.re, x⟩
theorem primitive_zeroAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(z₀ : ) :
(primitive z₀ f) z₀ = 0 := by
unfold primitive
simp
theorem primitive_fderivAtBasepointZero
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : Continuous f) :
HasDerivAt (primitive 0 f) (f 0) 0 := by
unfold primitive
simp
apply hasDerivAt_iff_isLittleO.2
simp
rw [Asymptotics.isLittleO_iff]
intro c hc
have {z : } {e : E} : z • e = (∫ (_ : ) in (0)..(z.re), e) + Complex.I • ∫ (_ : ) in (0)..(z.im), e:= by
simp
rw [smul_comm]
rw [← smul_assoc]
simp
have : z.re • e = (z.re : ) • e := by exact rfl
rw [this, ← add_smul]
simp
conv =>
left
intro x
left
arg 1
arg 2
rw [this]
have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
abel
have t₀ {r : } : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 r := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact hf
have : (fun x => ({ re := x, im := 0 } : )) = Complex.ofRealLI := by rfl
rw [this]
continuity
have t₁ {r : } : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 r := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact hf
fun_prop
have t₂ {a b : } : IntervalIntegrable (fun x_1 => f { re := a, im := x_1 }) MeasureTheory.volume 0 b := by
apply Continuous.intervalIntegrable
apply Continuous.comp hf
have : (Complex.mk a) = (fun x => Complex.I • Complex.ofRealCLM x + { re := a, im := 0 }) := by
funext x
apply Complex.ext
rw [Complex.add_re]
simp
simp
rw [this]
apply Continuous.add
continuity
fun_prop
have t₃ {a : } : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact hf
fun_prop
conv =>
left
intro x
left
arg 1
rw [this]
rw [← smul_sub]
rw [← intervalIntegral.integral_sub t₀ t₁]
rw [← intervalIntegral.integral_sub t₂ t₃]
rw [Filter.eventually_iff_exists_mem]
let s := f⁻¹' Metric.ball (f 0) (c / (4 : ))
have h₁s : IsOpen s := IsOpen.preimage hf Metric.isOpen_ball
have h₂s : 0 ∈ s := by
apply Set.mem_preimage.mpr
apply Metric.mem_ball_self
linarith
obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 h₁s 0 h₂s
have h₃ε : ∀ y ∈ Metric.ball 0 ε, ‖(f y) - (f 0)‖ < (c / (4 : )) := by
intro y hy
apply mem_ball_iff_norm.mp (h₂ε hy)
use Metric.ball 0 (ε / (4 : ))
constructor
· apply Metric.ball_mem_nhds 0
linarith
· intro y hy
have h₁y : |y.re| < ε / 4 := by
calc |y.re|
_ ≤ Complex.abs y := by apply Complex.abs_re_le_abs
_ < ε / 4 := by
let A := mem_ball_iff_norm.1 hy
simp at A
linarith
have h₂y : |y.im| < ε / 4 := by
calc |y.im|
_ ≤ Complex.abs y := by apply Complex.abs_im_le_abs
_ < ε / 4 := by
let A := mem_ball_iff_norm.1 hy
simp at A
linarith
have intervalComputation {x' y' : } (h : x' ∈ Ι 0 y') : |x'| ≤ |y'| := by
let A := h.1
let B := h.2
rcases le_total 0 y' with hy | hy
· simp [hy] at A
simp [hy] at B
rw [abs_of_nonneg hy]
rw [abs_of_nonneg (le_of_lt A)]
exact B
· simp [hy] at A
simp [hy] at B
rw [abs_of_nonpos hy]
rw [abs_of_nonpos]
linarith [h.1]
exact B
have t₁ : ‖(∫ (x : ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ ≤ (c / (4 : )) * |y.re - 0| := by
apply intervalIntegral.norm_integral_le_of_norm_le_const
intro x hx
have h₁x : |x| < ε / 4 := by
calc |x|
_ ≤ |y.re| := intervalComputation hx
_ < ε / 4 := h₁y
apply le_of_lt
apply h₃ε { re := x, im := 0 }
rw [mem_ball_iff_norm]
simp
have : { re := x, im := 0 } = (x : ) := by rfl
rw [this]
rw [Complex.abs_ofReal]
linarith
have t₂ : ‖∫ (x : ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ ≤ (c / (4 : )) * |y.im - 0| := by
apply intervalIntegral.norm_integral_le_of_norm_le_const
intro x hx
have h₁x : |x| < ε / 4 := by
calc |x|
_ ≤ |y.im| := intervalComputation hx
_ < ε / 4 := h₂y
apply le_of_lt
apply h₃ε { re := y.re, im := x }
simp
calc Complex.abs { re := y.re, im := x }
_ ≤ |y.re| + |x| := by
apply Complex.abs_le_abs_re_add_abs_im { re := y.re, im := x }
_ < ε := by
linarith
calc ‖(∫ (x : ) in (0)..(y.re), f { re := x, im := 0 } - f 0) + Complex.I • ∫ (x : ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖
_ ≤ ‖(∫ (x : ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖Complex.I • ∫ (x : ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
apply norm_add_le
_ ≤ ‖(∫ (x : ) in (0)..(y.re), f { re := x, im := 0 } - f 0)‖ + ‖∫ (x : ) in (0)..(y.im), f { re := y.re, im := x } - f 0‖ := by
simp
rw [norm_smul]
simp
_ ≤ (c / (4 : )) * |y.re - 0| + (c / (4 : )) * |y.im - 0| := by
apply add_le_add
exact t₁
exact t₂
_ ≤ (c / (4 : )) * (|y.re| + |y.im|) := by
simp
rw [mul_add]
_ ≤ (c / (4 : )) * (4 * ‖y‖) := by
have : |y.re| + |y.im| ≤ 4 * ‖y‖ := by
calc |y.re| + |y.im|
_ ≤ ‖y‖ + ‖y‖ := by
apply add_le_add
apply Complex.abs_re_le_abs
apply Complex.abs_im_le_abs
_ ≤ 4 * ‖y‖ := by
rw [← two_mul]
apply mul_le_mul
linarith
rfl
exact norm_nonneg y
linarith
apply mul_le_mul
rfl
exact this
apply add_nonneg
apply abs_nonneg
apply abs_nonneg
linarith
_ ≤ c * ‖y‖ := by
linarith
theorem primitive_translation
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(z₀ t : ) :
primitive z₀ (f ∘ fun z ↦ (z - t)) = ((primitive (z₀ - t) f) ∘ fun z ↦ (z - t)) := by
funext z
unfold primitive
simp
let g : → E := fun x ↦ f ( {re := x, im := z₀.im - t.im} )
have {x : } : f ({ re := x, im := z₀.im } - t) = g (1*x - t.re) := by
congr 1
apply Complex.ext <;> simp
conv =>
left
left
arg 1
intro x
rw [this]
rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.re)]
simp
congr 1
let g : → E := fun x ↦ f ( {re := z.re - t.re, im := x} )
have {x : } : f ({ re := z.re, im := x} - t) = g (1*x - t.im) := by
congr 1
apply Complex.ext <;> simp
conv =>
left
arg 1
intro x
rw [this]
rw [intervalIntegral.integral_comp_mul_sub g one_ne_zero (t.im)]
simp
theorem primitive_hasDerivAtBasepoint
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Continuous f)
(z₀ : ) :
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
let g := f ∘ fun z ↦ z + z₀
have : Continuous g := by continuity
let A := primitive_fderivAtBasepointZero g this
simp at A
let B := primitive_translation g z₀ z₀
simp at B
have : (g ∘ fun z ↦ (z - z₀)) = f := by
funext z
dsimp [g]
simp
rw [this] at B
rw [B]
have : f z₀ = (1 : ) • (f z₀) := by
exact (MulAction.one_smul (f z₀)).symm
conv =>
arg 2
rw [this]
apply HasDerivAt.scomp
simp
have : g 0 = f z₀ := by simp [g]
rw [← this]
exact A
apply HasDerivAt.sub_const
have : (fun (x : ) ↦ x) = id := by
funext x
simp
rw [this]
exact hasDerivAt_id z₀
lemma integrability₁
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : Differentiable f)
(a₁ a₂ b : ) :
IntervalIntegrable (fun x => f { re := x, im := b }) MeasureTheory.volume a₁ a₂ := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact Differentiable.continuous hf
have : ((fun x => { re := x, im := b }) : ) = (fun x => Complex.ofRealCLM x + { re := 0, im := b }) := by
funext x
apply Complex.ext
rw [Complex.add_re]
simp
rw [Complex.add_im]
simp
rw [this]
continuity
lemma integrability₂
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : Differentiable f)
(a₁ a₂ b : ) :
IntervalIntegrable (fun x => f { re := b, im := x }) MeasureTheory.volume a₁ a₂ := by
apply Continuous.intervalIntegrable
apply Continuous.comp
exact Differentiable.continuous hf
have : (Complex.mk b) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
funext x
apply Complex.ext
rw [Complex.add_re]
simp
simp
rw [this]
apply Continuous.add
continuity
fun_prop
theorem primitive_additivity
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : Differentiable f)
(z₀ z₁ : ) :
(fun z ↦ (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁)) = 0 := by
funext z
unfold primitive
have : (∫ (x : ) in z₀.re..z.re, f { re := x, im := z₀.im }) = (∫ (x : ) in z₀.re..z₁.re, f { re := x, im := z₀.im }) + (∫ (x : ) in z₁.re..z.re, f { re := x, im := z₀.im }) := by
rw [intervalIntegral.integral_add_adjacent_intervals]
apply integrability₁ f hf
apply integrability₁ f hf
rw [this]
have : (∫ (x : ) in z₀.im..z.im, f { re := z.re, im := x }) = (∫ (x : ) in z₀.im..z₁.im, f { re := z.re, im := x }) + (∫ (x : ) in z₁.im..z.im, f { re := z.re, im := x }) := by
rw [intervalIntegral.integral_add_adjacent_intervals]
apply integrability₂ f hf
apply integrability₂ f hf
rw [this]
simp
have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d - h + (c) := by
abel
rw [this]
simp
let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ (hf.differentiableOn)
have {x : } {w : } : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
apply Complex.ext
· simp
· simp
simp_rw [this] at A
have {x : } {w : } : w.re + x * Complex.I = { re := w.re, im := x } := by
apply Complex.ext
· simp
· simp
simp_rw [this] at A
rw [← A]
abel
theorem primitive_additivity'
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
(f : → E)
(hf : Differentiable f)
(z₀ z₁ : ) :
primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := by
nth_rw 1 [← sub_zero (primitive z₀ f)]
rw [← primitive_additivity f hf z₀ z₁]
funext z
simp
abel
theorem primitive_hasDerivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ z : ) :
HasDerivAt (primitive z₀ f) (f z) z := by
rw [primitive_additivity' f hf z₀ z]
rw [← add_zero (f z)]
apply HasDerivAt.add
apply primitive_hasDerivAtBasepoint
exact hf.continuous
apply hasDerivAt_const
theorem primitive_differentiable
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
Differentiable (primitive z₀ f) := by
intro z
exact (primitive_hasDerivAt hf z₀ z).differentiableAt
theorem primitive_hasFderivAt
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ).flip (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_hasFderivAt'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul (f z)) z := by
intro z
rw [hasFDerivAt_iff_hasDerivAt]
simp
exact primitive_hasDerivAt hf z₀ z
theorem primitive_fderiv
{E : Type u} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E]
{f : → E}
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ).flip (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt hf z₀ z
theorem primitive_fderiv'
{f : }
(hf : Differentiable f)
(z₀ : ) :
∀ z, (fderiv (primitive z₀ f) z) = ContinuousLinearMap.lsmul (f z) := by
intro z
apply HasFDerivAt.fderiv
exact primitive_hasFderivAt' hf z₀ z

View File

@ -5,7 +5,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592",
"rev": "0f3e143dffdc3a591662f3401ce1d7a3405227c0",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -25,7 +25,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
"rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@ -35,27 +35,27 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "d1b33202c3a29a079f292de65ea438648123b635",
"rev": "c87908619cccadda23f71262e6898b9893bffa36",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.39",
"inputRev": "v0.0.40",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"scope": "",
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
"rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/import-graph",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
"rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -65,7 +65,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "cc495260156b40dcbd55b947c047061e15344000",
"rev": "c96401c7496392a2200dc78c0b334df0561466dc",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,

View File

@ -1 +1 @@
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.10.0