diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean index 0be7e3a..d5fea68 100644 --- a/Nevanlinna/analyticAt.lean +++ b/Nevanlinna/analyticAt.lean @@ -1,5 +1,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros import Mathlib.Analysis.Complex.Basic +import Mathlib.Analysis.Analytic.Linear theorem AnalyticAt.order_mul @@ -85,3 +86,97 @@ theorem AnalyticAt.supp_order_toNat contrapose intro h₁f simp [hf.order_eq_zero_iff.2 h₁f] + + +theorem ContinuousLinearEquiv.analyticAt + (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀ + + +theorem eventually_nhds_comp_composition + {f₁ f₂ ℓ : ℂ → ℂ} + {z₀ : ℂ} + (hf : ∀ᶠ (z : ℂ) in nhds (ℓ z₀), f₁ z = f₂ z) + (hℓ : Continuous ℓ) : + ∀ᶠ (z : ℂ) in nhds z₀, (f₁ ∘ ℓ) z = (f₂ ∘ ℓ) z := by + obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hf + apply eventually_nhds_iff.2 + use ℓ⁻¹' t + constructor + · intro y hy + exact h₁t (ℓ y) hy + · constructor + · apply IsOpen.preimage + exact ContinuousLinearEquiv.continuous ℓ + exact h₂t + · exact h₃t + + +theorem AnalyticAt.order_congr + {f₁ f₂ : ℂ → ℂ} + {z₀ : ℂ} + (hf₁ : AnalyticAt ℂ f₁ z₀) + (hf₂ : AnalyticAt ℂ f₂ z₀) + (hf : ∀ᶠ (z : ℂ) in nhds z₀, f₁ z = f₂ z) : + hf₁.order = hf₂.order := by + + sorry + + +theorem AnalyticAt.order_comp_CLE + (ℓ : ℂ ≃L[ℂ] ℂ) + {f : ℂ → ℂ} + {z₀ : ℂ} + (hf : AnalyticAt ℂ f (ℓ z₀)) : + hf.order = (hf.comp (ℓ.analyticAt z₀)).order := by + + by_cases h₁f : hf.order = ⊤ + · rw [h₁f] + rw [AnalyticAt.order_eq_top_iff] at h₁f + let A := eventually_nhds_comp_composition h₁f ℓ.continuous + simp at A + have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by apply analyticAt_const + rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A] + + have : this.order = ⊤ := by + rw [AnalyticAt.order_eq_top_iff] + simp + rw [this] + · let n := hf.order.toNat + have hn : hf.order = n := Eq.symm (ENat.coe_toNat h₁f) + rw [hn] + rw [AnalyticAt.order_eq_nat_iff] at hn + obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn + have A := eventually_nhds_comp_composition h₃g ℓ.continuous + simp only [Function.comp_apply] at A + have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by apply analyticAt_const + rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) this A] + simp + rw [AnalyticAt.order_mul] + + + + + --rw [hn, AnalyticAt.order_eq_nat_iff] + rw [AnalyticAt.order_eq_nat_iff] at hn + obtain ⟨g, h₁g, h₂g, h₃g⟩ := hn + use g ∘ ℓ + constructor + · exact h₁g.comp (ℓ.analyticAt z₀) + · constructor + · exact h₂g + · rw [eventually_nhds_iff] + rw [eventually_nhds_iff] at h₃g + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃g + use ℓ⁻¹' t + constructor + · intro y hy + simp + rw [h₁t (ℓ y) hy] + + + sorry + · constructor + · apply IsOpen.preimage + exact ContinuousLinearEquiv.continuous ℓ + exact h₂t + · exact h₃t diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index b446012..e1601e9 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -11,7 +11,7 @@ open Real theorem jensen_case_R_eq_one (f : ℂ → ℂ) - (h₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1)) + (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1)) (h₂f : f 0 ≠ 0) : log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by @@ -284,3 +284,103 @@ theorem jensen_case_R_eq_one simp apply h₂F simp + + +lemma const_mul_circleMap_zero + {R θ : ℝ} : + circleMap 0 R θ = R * circleMap 0 1 θ := by + rw [circleMap_zero, circleMap_zero] + simp + + +theorem jensen + {R : ℝ} + (hR : 0 < R) + (f : ℂ → ℂ) + (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R)) + (h₂f : f 0 ≠ 0) : + log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by + + let F := fun z ↦ f (R • z) + + + + have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by + apply AnalyticOn.comp (t := Metric.closedBall 0 R) + exact h₁f + + + + sorry + have h₂F : F 0 ≠ 0 := by sorry + + let A := jensen_case_R_eq_one F h₁F h₂F + dsimp [F] at A + simp + rw [mul_zero] at A + rw [A] + simp + + simp_rw [← const_mul_circleMap_zero] + simp + + let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by + intro ⟨x, hx⟩ + have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by + simp + simp at hx + have : R = |R| := by exact Eq.symm (abs_of_pos hR) + rw [← this] + norm_num + calc R * Complex.abs x + _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx + _ = R := by simp + exact ⟨R • x, hy⟩ + + let e' : (Metric.closedBall (0 : ℂ) R) → (Metric.closedBall (0 : ℂ) 1) := by + intro ⟨x, hx⟩ + have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ℂ) 1 := by + simp + simp at hx + have : R = |R| := by exact Eq.symm (abs_of_pos hR) + rw [← this] + norm_num + calc R⁻¹ * Complex.abs x + _ ≤ R⁻¹ * R := by + apply mul_le_mul_of_nonneg_left hx + apply inv_nonneg.mpr + exact abs_eq_self.mp (id (Eq.symm this)) + _ = 1 := by + apply inv_mul_cancel₀ + exact Ne.symm (ne_of_lt hR) + exact ⟨R⁻¹ • x, hy⟩ + + apply finsum_eq_of_bijective e + + apply Function.bijective_iff_has_inverse.mpr + use e' + constructor + · apply Function.leftInverse_iff_comp.mpr + funext x + dsimp only [e, e', id_eq, eq_mp_eq_cast, Function.comp_apply] + conv => + left + arg 1 + rw [← smul_assoc, smul_eq_mul] + rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))] + rw [one_smul] + · apply Function.rightInverse_iff_comp.mpr + funext x + dsimp only [e, e', id_eq, eq_mp_eq_cast, Function.comp_apply] + conv => + left + arg 1 + rw [← smul_assoc, smul_eq_mul] + rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))] + rw [one_smul] + + intro x + simp + + + sorry