Jensen's formula is done!

This commit is contained in:
Stefan Kebekus 2024-09-12 08:56:01 +02:00
parent 5a984253c6
commit 712be956d0
1 changed files with 28 additions and 2 deletions

View File

@ -350,6 +350,7 @@ theorem jensen
simpa
let A := jensen_case_R_eq_one F h₁F h₂F
dsimp [F] at A
have {x : } : x = R * x := by rfl
repeat
@ -357,7 +358,6 @@ theorem jensen
simp at A
simp
rw [A]
simp_rw [← const_mul_circleMap_zero]
simp
@ -394,6 +394,7 @@ theorem jensen
apply finsum_eq_of_bijective e
apply Function.bijective_iff_has_inverse.mpr
use e'
constructor
@ -418,6 +419,31 @@ theorem jensen
intro x
simp
by_cases hx : x = (0 : )
rw [hx]
simp
rw [log_mul, log_mul, log_inv, log_inv]
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
simp
left
congr 1
sorry
dsimp [AnalyticOn.order]
rw [← AnalyticAt.order_comp_CLE ]
--
simpa
--
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
rw [← this]
apply inv_ne_zero
exact Ne.symm (ne_of_lt hR)
--
exact Ne.symm (ne_of_lt hR)
--
simp
constructor
· assumption
· exact Ne.symm (ne_of_lt hR)