From f5a835764b002dfdd846008ff42944d1dec0590a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 3 Jan 2025 17:45:22 +0100 Subject: [PATCH] Update --- Nevanlinna.lean | 29 +- Nevanlinna/analyticOnNhd_divisor.lean | 59 -- Nevanlinna/analyticOnNhd_zeroSet.lean | 461 ------------ Nevanlinna/bilinear.lean | 77 -- Nevanlinna/diffOp.lean | 104 --- Nevanlinna/holomorphic.lean | 176 ----- Nevanlinna/holomorphic_zero.lean | 358 ---------- .../junk/holomorphic_JensenFormula.lean | 449 ------------ Nevanlinna/junk/holomorphic_primitive.lean | 666 ------------------ Nevanlinna/junk/laplace2.lean | 285 -------- .../stronglyMeromorphic_JensenFormula_1.lean | 528 -------------- Nevanlinna/specialFunctions_Integral_log.lean | 65 -- lake-manifest.json | 2 +- 13 files changed, 29 insertions(+), 3230 deletions(-) delete mode 100644 Nevanlinna/analyticOnNhd_divisor.lean delete mode 100644 Nevanlinna/analyticOnNhd_zeroSet.lean delete mode 100644 Nevanlinna/bilinear.lean delete mode 100644 Nevanlinna/diffOp.lean delete mode 100644 Nevanlinna/holomorphic.lean delete mode 100644 Nevanlinna/holomorphic_zero.lean delete mode 100644 Nevanlinna/junk/holomorphic_JensenFormula.lean delete mode 100644 Nevanlinna/junk/holomorphic_primitive.lean delete mode 100644 Nevanlinna/junk/laplace2.lean delete mode 100644 Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean delete mode 100644 Nevanlinna/specialFunctions_Integral_log.lean diff --git a/Nevanlinna.lean b/Nevanlinna.lean index eba18bb..026a3be 100644 --- a/Nevanlinna.lean +++ b/Nevanlinna.lean @@ -1 +1,28 @@ -import Nevanlinna.cauchyRiemann \ No newline at end of file +import Nevanlinna.analyticAt +import Nevanlinna.cauchyRiemann +import Nevanlinna.codiscreteWithin +import Nevanlinna.divisor +import Nevanlinna.firstMain +import Nevanlinna.harmonicAt +import Nevanlinna.harmonicAt_examples +import Nevanlinna.harmonicAt_meanValue +import Nevanlinna.holomorphicAt +import Nevanlinna.holomorphic_examples +import Nevanlinna.holomorphic_primitive +import Nevanlinna.intervalIntegrability +import Nevanlinna.laplace +import Nevanlinna.logpos +import Nevanlinna.mathlibAddOn +import Nevanlinna.meromorphicAt +import Nevanlinna.meromorphicOn +import Nevanlinna.meromorphicOn_divisor +import Nevanlinna.meromorphicOn_integrability +import Nevanlinna.partialDeriv +import Nevanlinna.periodic_integrability +import Nevanlinna.specialFunctions_CircleIntegral_affine +import Nevanlinna.specialFunctions_Integral_log_sin +import Nevanlinna.stronglyMeromorphicAt +import Nevanlinna.stronglyMeromorphicOn +import Nevanlinna.stronglyMeromorphicOn_eliminate +import Nevanlinna.stronglyMeromorphicOn_ratlPolynomial +import Nevanlinna.stronglyMeromorphic_JensenFormula diff --git a/Nevanlinna/analyticOnNhd_divisor.lean b/Nevanlinna/analyticOnNhd_divisor.lean deleted file mode 100644 index a7a2623..0000000 --- a/Nevanlinna/analyticOnNhd_divisor.lean +++ /dev/null @@ -1,59 +0,0 @@ -import Nevanlinna.analyticAt -import Nevanlinna.divisor - -open scoped Interval Topology -open Real Filter MeasureTheory intervalIntegral - - -noncomputable def AnalyticOnNhd.zeroDivisor - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOnNhd ℂ f U) : - Divisor U where - - toFun := by - intro z - if hz : z ∈ U then - exact ((hf z hz).order.toNat : ℤ) - else - exact 0 - - supportInU := by - intro z hz - simp at hz - by_contra h₂z - simp [h₂z] at hz - - locallyFiniteInU := by - intro z hz - - apply eventually_nhdsWithin_iff.2 - rw [eventually_nhds_iff] - - rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h - · rw [eventually_nhds_iff] at h - obtain ⟨N, h₁N, h₂N, h₃N⟩ := h - use N - constructor - · intro y h₁y _ - by_cases h₃y : y ∈ U - · simp [h₃y] - right - rw [AnalyticAt.order_eq_top_iff (hf y h₃y)] - rw [eventually_nhds_iff] - use N - · simp [h₃y] - · tauto - - · rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h - obtain ⟨N, h₁N, h₂N, h₃N⟩ := h - use N - constructor - · intro y h₁y h₂y - by_cases h₃y : y ∈ U - · simp [h₃y] - left - rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)] - exact h₁N y h₁y h₂y - · simp [h₃y] - · tauto diff --git a/Nevanlinna/analyticOnNhd_zeroSet.lean b/Nevanlinna/analyticOnNhd_zeroSet.lean deleted file mode 100644 index df14a9d..0000000 --- a/Nevanlinna/analyticOnNhd_zeroSet.lean +++ /dev/null @@ -1,461 +0,0 @@ -import Mathlib.Analysis.Analytic.Constructions -import Mathlib.Analysis.Analytic.IsolatedZeros -import Mathlib.Analysis.Complex.Basic -import Nevanlinna.analyticAt - - -noncomputable def AnalyticOnNhd.order - {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order - - -theorem AnalyticOnNhd.order_eq_nat_iff - {f : ℂ → ℂ} - {U : Set ℂ} - {z₀ : U} - (hf : AnalyticOnNhd ℂ f U) - (n : ℕ) : - hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by - - constructor - -- Direction → - intro hn - obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ z₀.2) n).1 hn - - -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the - -- removable singularity removed - let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n - - -- Describe g near z₀ - have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by - rw [eventually_nhds_iff] - obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc - use t - constructor - · intro y h₁y - by_cases h₂y : y = z₀ - · dsimp [g]; simp [h₂y] - · dsimp [g]; simp [h₂y] - rw [div_eq_iff_mul_eq, eq_comm, mul_comm] - exact h₁t y h₁y - norm_num - rw [sub_eq_zero] - tauto - · constructor - · assumption - · assumption - - -- Describe g near points z₁ that are different from z₀ - have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by - intro hz₁ - rw [eventually_nhds_iff] - use {z₀.1}ᶜ - constructor - · intro y hy - simp at hy - simp [g, hy] - · exact ⟨isOpen_compl_singleton, hz₁⟩ - - -- Use g and show that it has all required properties - use g - constructor - · -- AnalyticOn ℂ g U - intro z h₁z - by_cases h₂z : z = z₀ - · rw [h₂z] - apply AnalyticAt.congr h₁gloc - exact Filter.EventuallyEq.symm g_near_z₀ - · simp_rw [eq_comm] at g_near_z₁ - apply AnalyticAt.congr _ (g_near_z₁ h₂z) - apply AnalyticAt.div - exact hf z h₁z - apply AnalyticAt.pow - apply AnalyticAt.sub - apply analyticAt_id - apply analyticAt_const - simp - rw [sub_eq_zero] - tauto - · constructor - · simp [g]; tauto - · intro z - by_cases h₂z : z = z₀ - · rw [h₂z, g_near_z₀.self_of_nhds] - exact h₃gloc.self_of_nhds - · rw [(g_near_z₁ h₂z).self_of_nhds] - simp [h₂z] - rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀] - simp; norm_num - rw [sub_eq_zero] - tauto - - -- direction ← - intro h - obtain ⟨g, h₁g, h₂g, h₃g⟩ := h - dsimp [AnalyticOnNhd.order] - rw [AnalyticAt.order_eq_nat_iff] - use g - exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ - - -theorem AnalyticOnNhd.support_of_order₁ - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOnNhd ℂ f U) : - Function.support hf.order = U.restrict f⁻¹' {0} := by - ext u - simp [AnalyticOnNhd.order] - rw [not_iff_comm, (hf u u.2).order_eq_zero_iff] - - -theorem AnalyticOnNhd.eliminateZeros - {f : ℂ → ℂ} - {U : Set ℂ} - {A : Finset U} - (hf : AnalyticOnNhd ℂ f U) - (n : U → ℕ) : - (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by - - apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z) - - -- case empty - simp - use f - simp - exact hf - - -- case insert - intro b₀ B hb iHyp - intro hBinsert - obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha)) - - have : (h₁g₀ b₀ b₀.2).order = n b₀ := by - - rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)] - - let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a) - - have : f = fun z ↦ φ z * g₀ z := by - funext z - rw [h₃g₀ z] - rfl - simp_rw [this] - - have h₁φ : AnalyticAt ℂ φ b₀ := by - dsimp [φ] - apply Finset.analyticAt_prod - intro b _ - apply AnalyticAt.pow - apply AnalyticAt.sub - apply analyticAt_id - exact analyticAt_const - - have h₂φ : h₁φ.order = (0 : ℕ) := by - rw [AnalyticAt.order_eq_nat_iff h₁φ 0] - use φ - constructor - · assumption - · constructor - · dsimp [φ] - push_neg - rw [Finset.prod_ne_zero_iff] - intro a ha - simp - have : ¬ (b₀.1 - a.1 = 0) := by - by_contra C - rw [sub_eq_zero] at C - rw [SetCoe.ext C] at hb - tauto - tauto - · simp - - rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)] - - rw [h₂φ] - simp - - obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (n b₀)).1 this - - use g₁ - constructor - · exact h₁g₁ - · constructor - · intro a h₁a - by_cases h₂a : a = b₀ - · rwa [h₂a] - · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a - let B' := h₃g₁ a - let C' := h₂g₀ a A' - rw [B'] at C' - exact right_ne_zero_of_smul C' - · intro z - let A' := h₃g₀ z - rw [h₃g₁ z] at A' - rw [A'] - rw [← smul_assoc] - congr - simp - rw [Finset.prod_insert] - ring - exact hb - - -theorem XX - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by - - intro hu - apply ENat.coe_toNat - by_contra C - rw [(h₁f u hu).order_eq_top_iff] at C - rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C - obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f - rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁ - tauto - - -theorem discreteZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - DiscreteTopology ((U.restrict f)⁻¹' {0}) := by - - simp_rw [← singletons_open_iff_discrete] - simp_rw [Metric.isOpen_singleton_iff] - - intro z - - let A := XX hU h₁f h₂f z.1.2 - rw [eq_comm] at A - rw [AnalyticAt.order_eq_nat_iff] at A - obtain ⟨g, h₁g, h₂g, h₃g⟩ := A - - rw [Metric.eventually_nhds_iff_ball] at h₃g - have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by - have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g - have : {0}ᶜ ∈ nhds (g z) := by - exact compl_singleton_mem_nhds_iff.mpr h₂g - - let F := h₄g.preimage_mem_nhds this - rw [Metric.mem_nhds_iff] at F - obtain ⟨ε, h₁ε, h₂ε⟩ := F - use ε - constructor; exact h₁ε - intro y hy - let G := h₂ε hy - simp at G - exact G - obtain ⟨ε₁, h₁ε₁⟩ := this - - obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g - use min ε₁ ε₂ - constructor - · have : 0 < min ε₁ ε₂ := by - rw [lt_min_iff] - exact And.imp_right (fun _ => h₁ε₂) h₁ε₁ - exact this - - intro y - intro h₁y - - have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ - - have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ - - have F := h₂ε₂ y.1 h₂y - have : f y = 0 := by exact y.2 - rw [this] at F - simp at F - - have : g y.1 ≠ 0 := by - exact h₁ε₁.2 y h₃y - simp [this] at F - ext - rw [sub_eq_zero] at F - tauto - - -theorem finiteZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - Set.Finite (U.restrict f⁻¹' {0}) := by - - have closedness : IsClosed (U.restrict f⁻¹' {0}) := by - apply IsClosed.preimage - apply continuousOn_iff_continuous_restrict.1 - exact h₁f.continuousOn - exact isClosed_singleton - - have : CompactSpace U := by - exact isCompact_iff_compactSpace.mp h₂U - - apply (IsClosed.isCompact closedness).finite - exact discreteZeros h₁U h₁f h₂f - - -theorem AnalyticOnNhdCompact.eliminateZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by - - let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset - - let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat - - have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by - intro a _ - dsimp [n, AnalyticOnNhd.order] - rw [eq_comm] - apply XX h₁U - exact h₂f - - - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn - use g - use A - - have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by - intro z - rw [h₃g z] - - constructor - · exact h₁g - · constructor - · intro z h₁z - by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet - · exact h₂g ⟨z, h₁z⟩ h₂z - · have : f z ≠ 0 := by - by_contra C - have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by - dsimp [A] - simp - exact C - tauto - rw [inter z] at this - exact right_ne_zero_of_smul this - · exact inter - - -theorem AnalyticOnNhdCompact.eliminateZeros₂ - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by - - let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset - - let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat - - have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by - intro a _ - dsimp [n, AnalyticOnNhd.order] - rw [eq_comm] - apply XX h₁U - exact h₂f - - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn - use g - - have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by - intro z - rw [h₃g z] - - constructor - · exact h₁g - · constructor - · intro z h₁z - by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet - · exact h₂g ⟨z, h₁z⟩ h₂z - · have : f z ≠ 0 := by - by_contra C - have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by - dsimp [A] - simp - exact C - tauto - rw [inter z] at this - exact right_ne_zero_of_smul this - · exact h₃g - - -theorem AnalyticOnNhdCompact.eliminateZeros₁ - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by - - let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset - - let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat - - have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by - intro a _ - dsimp [n, AnalyticOnNhd.order] - rw [eq_comm] - apply XX h₁U - exact h₂f - - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn - use g - - have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by - intro z - rw [h₃g z] - - constructor - · exact h₁g - · constructor - · intro z h₁z - by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet - · exact h₂g ⟨z, h₁z⟩ h₂z - · have : f z ≠ 0 := by - by_contra C - have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by - dsimp [A] - simp - exact C - tauto - rw [inter z] at this - exact right_ne_zero_of_smul this - · intro z - - let φ : U → ℂ := fun a ↦ (z - ↑a) ^ (h₁f.order a).toNat - have hφ : Function.mulSupport φ ⊆ A := by - intro x hx - simp [φ] at hx - have : (h₁f.order x).toNat ≠ 0 := by - by_contra C - rw [C] at hx - simp at hx - simp [A] - exact AnalyticAt.supp_order_toNat (h₁f x x.2) this - rw [finprod_eq_prod_of_mulSupport_subset φ hφ] - rw [inter z] - rfl diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean deleted file mode 100644 index 533b209..0000000 --- a/Nevanlinna/bilinear.lean +++ /dev/null @@ -1,77 +0,0 @@ -/- -Copyright (c) 2024 Stefan Kebekus. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Stefan Kebekus --/ - -import Mathlib.Analysis.InnerProductSpace.PiL2 - -/-! - -# Canoncial Elements in Tensor Powers of Real Inner Product Spaces - -Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors, which -are relevant when for a coordinate-free definition of differential operators -such as the Laplacian. - -* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is - the element corresponding to the inner product. - -* If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its - dual. Accordingly, there exists an element - `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` that corresponds to - `InnerProductSpace.canonicalContravariantTensor E` under this identification. - -The theorem `InnerProductSpace.canonicalCovariantTensorRepresentation` shows -that `InnerProductSpace.canonicalCovariantTensor E` can be computed from any -orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`. - --/ - -open InnerProductSpace -open TensorProduct - - -noncomputable def InnerProductSpace.canonicalContravariantTensor - {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] - : E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner - - -noncomputable def InnerProductSpace.canonicalCovariantTensor - (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] - : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i) - -theorem InnerProductSpace.canonicalCovariantTensorRepresentation - (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] - [Fintype ι] - (v : OrthonormalBasis ι ℝ E) : - InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by - - let w := stdOrthonormalBasis ℝ E - conv => - right - arg 2 - intro i - rw [← w.sum_repr' (v i)] - simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul] - - conv => - right - rw [Finset.sum_comm] - arg 2 - intro y - rw [Finset.sum_comm] - arg 2 - intro x - rw [← Finset.sum_smul] - arg 1 - arg 2 - intro i - rw [← real_inner_comm (w x)] - simp_rw [OrthonormalBasis.sum_inner_mul_inner v] - - have {i} : ∑ j, ⟪w i, w j⟫_ℝ • w i ⊗ₜ[ℝ] w j = w i ⊗ₜ[ℝ] w i := by - rw [Fintype.sum_eq_single i, orthonormal_iff_ite.1 w.orthonormal]; simp - intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto - simp_rw [this] - rfl diff --git a/Nevanlinna/diffOp.lean b/Nevanlinna/diffOp.lean deleted file mode 100644 index 1d25981..0000000 --- a/Nevanlinna/diffOp.lean +++ /dev/null @@ -1,104 +0,0 @@ -import Mathlib.Analysis.Calculus.ContDiff.Basic -import Mathlib.Analysis.InnerProductSpace.PiL2 - -/- - -Let E, F, G be vector spaces over nontrivally normed field 𝕜, a homogeneus -linear differential operator of order n is a map that attaches to every point e -of E a linear evaluation - -{Continuous 𝕜-multilinear maps E → F in n variables} → G - -In other words, homogeneus linear differential operator of order n is an -instance of the type: - -D : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G - -Given any map f : E → F, one obtains a map D f : E → G by sending a point e to -the evaluation (D e), applied to the n.th derivative of f at e - -fun e ↦ D e (iteratedFDeriv 𝕜 n f e) - --/ - -@[ext] -class HomLinDiffOp - (𝕜 : Type*) [NontriviallyNormedField 𝕜] - (n : ℕ) - (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] - (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F] - (G : Type*) [NormedAddCommGroup G] [NormedSpace 𝕜 G] -where - tensorfield : E → ( E [×n]→L[𝕜] F) →L[𝕜] G --- tensorfield : E → (ContinuousMultilinearMap 𝕜 (fun _ : Fin n ↦ E) F) →ₗ[𝕜] G - - -namespace HomLinDiffOp - -noncomputable def toFun - {𝕜 : Type*} [NontriviallyNormedField 𝕜] - {n : ℕ} - {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] - {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] - (o : HomLinDiffOp 𝕜 n E F G) - : (E → F) → (E → G) := - fun f z ↦ o.tensorfield z (iteratedFDeriv 𝕜 n f z) - - -noncomputable def Laplace - {𝕜 : Type*} [RCLike 𝕜] - {n : ℕ} - : HomLinDiffOp 𝕜 2 (EuclideanSpace 𝕜 (Fin n)) 𝕜 𝕜 - where - tensorfield := by - intro _ - - let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n)) - rw [finrank_euclideanSpace_fin] at v - - exact { - toFun := fun f' ↦ ∑ i, f' ![v i, v i] - map_add' := by - intro f₁ f₂ - exact Finset.sum_add_distrib - map_smul' := by - intro m f - exact Eq.symm (Finset.mul_sum Finset.univ (fun i ↦ f ![v i, v i]) m) - cont := by - simp - apply continuous_finset_sum - intro i _ - exact ContinuousMultilinearMap.continuous_eval_const ![v i, v i] - } - - -noncomputable def Gradient - {𝕜 : Type*} [RCLike 𝕜] - {n : ℕ} - : HomLinDiffOp 𝕜 1 (EuclideanSpace 𝕜 (Fin n)) 𝕜 (EuclideanSpace 𝕜 (Fin n)) - where - tensorfield := by - intro _ - - let v := stdOrthonormalBasis 𝕜 (EuclideanSpace 𝕜 (Fin n)) - rw [finrank_euclideanSpace_fin] at v - - exact { - toFun := fun f' ↦ ∑ i, (f' ![v i]) • (v i) - map_add' := by - intro f₁ f₂ - simp; simp_rw [add_smul, Finset.sum_add_distrib] - map_smul' := by - intro m f - simp; simp_rw [Finset.smul_sum, ←smul_assoc,smul_eq_mul] - cont := by - simp - apply continuous_finset_sum - intro i _ - apply Continuous.smul - exact ContinuousMultilinearMap.continuous_eval_const ![v i] - exact continuous_const - } - -end HomLinDiffOp diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean deleted file mode 100644 index 93e6672..0000000 --- a/Nevanlinna/holomorphic.lean +++ /dev/null @@ -1,176 +0,0 @@ -import Mathlib.Analysis.Complex.TaylorSeries -import Nevanlinna.cauchyRiemann - -variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] -variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] - -def HolomorphicAt (f : E → F) (x : E) : Prop := - ∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z - - -theorem HolomorphicAt_iff - {f : E → F} - {x : E} : - HolomorphicAt f x ↔ ∃ s : - Set E, IsOpen s ∧ x ∈ s ∧ (∀ z ∈ s, DifferentiableAt ℂ f z) := by - constructor - · intro hf - obtain ⟨t, h₁t, h₂t⟩ := hf - obtain ⟨s, h₁s, h₂s, h₃s⟩ := mem_nhds_iff.1 h₁t - use s - constructor - · assumption - · constructor - · assumption - · intro z hz - exact h₂t z (h₁s hz) - · intro hyp - obtain ⟨s, h₁s, h₂s, hf⟩ := hyp - use s - constructor - · apply (IsOpen.mem_nhds_iff h₁s).2 h₂s - · assumption - - -theorem HolomorphicAt_analyticAt - [CompleteSpace F] - {f : ℂ → F} - {x : ℂ} : - HolomorphicAt f x → AnalyticAt ℂ f x := by - intro hf - obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf - apply DifferentiableOn.analyticAt (s := s) - intro z hz - apply DifferentiableAt.differentiableWithinAt - apply h₃s - exact hz - exact IsOpen.mem_nhds h₁s h₂s - - -theorem HolomorphicAt_differentiableAt - {f : E → F} - {x : E} : - HolomorphicAt f x → DifferentiableAt ℂ f x := by - intro hf - obtain ⟨s, _, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hf - exact h₃s x h₂s - - -theorem HolomorphicAt_isOpen - (f : E → F) : - IsOpen { x : E | HolomorphicAt f x } := by - - rw [← subset_interior_iff_isOpen] - intro x hx - simp at hx - obtain ⟨s, h₁s, h₂s, h₃s⟩ := HolomorphicAt_iff.1 hx - use s - constructor - · simp - constructor - · exact h₁s - · intro x hx - simp - use s - constructor - · exact IsOpen.mem_nhds h₁s hx - · exact h₃s - · exact h₂s - - -theorem HolomorphicAt_comp - {g : E → F} - {f : F → G} - {z : E} - (hf : HolomorphicAt f (g z)) - (hg : HolomorphicAt g z) : - HolomorphicAt (f ∘ g) z := by - obtain ⟨UE, h₁UE, h₂UE⟩ := hg - obtain ⟨UF, h₁UF, h₂UF⟩ := hf - use UE ∩ g⁻¹' UF - constructor - · simp - constructor - · assumption - · apply ContinuousAt.preimage_mem_nhds - apply (h₂UE z (mem_of_mem_nhds h₁UE)).continuousAt - assumption - · intro x hx - apply DifferentiableAt.comp - apply h₂UF - exact hx.2 - apply h₂UE - exact hx.1 - - -theorem HolomorphicAt_neg - {f : E → F} - {z : E} - (hf : HolomorphicAt f z) : - HolomorphicAt (-f) z := by - obtain ⟨UF, h₁UF, h₂UF⟩ := hf - use UF - constructor - · assumption - · intro z hz - apply differentiableAt_neg_iff.mp - simp - exact h₂UF z hz - - -theorem HolomorphicAt_contDiffAt - [CompleteSpace F] - {f : ℂ → F} - {z : ℂ} - (hf : HolomorphicAt f z) : - ContDiffAt ℝ 2 f z := by - - let t := {x | HolomorphicAt f x} - have ht : IsOpen t := HolomorphicAt_isOpen f - have hz : z ∈ t := by exact hf - - -- ContDiffAt ℝ 2 f z - apply ContDiffOn.contDiffAt _ ((IsOpen.mem_nhds_iff ht).2 hz) - suffices h : ContDiffOn ℂ 2 f t from by - apply ContDiffOn.restrict_scalars ℝ h - apply DifferentiableOn.contDiffOn _ ht - intro w hw - apply DifferentiableAt.differentiableWithinAt - exact HolomorphicAt_differentiableAt hw - - -theorem CauchyRiemann'₅ - {f : ℂ → F} - {z : ℂ} - (h : DifferentiableAt ℂ f z) : - partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by - unfold partialDeriv - - conv => - left - rw [DifferentiableAt.fderiv_restrictScalars ℝ h] - simp - rw [← mul_one Complex.I] - rw [← smul_eq_mul] - conv => - right - right - rw [DifferentiableAt.fderiv_restrictScalars ℝ h] - simp - -theorem CauchyRiemann'₆ - {f : ℂ → F} - {z : ℂ} - (h : HolomorphicAt f z) : - partialDeriv ℝ Complex.I f =ᶠ[nhds z] Complex.I • partialDeriv ℝ 1 f := by - - obtain ⟨s, h₁s, hz, h₂f⟩ := HolomorphicAt_iff.1 h - - apply Filter.eventuallyEq_iff_exists_mem.2 - use s - constructor - · exact IsOpen.mem_nhds h₁s hz - · intro w hw - apply CauchyRiemann'₅ - exact h₂f w hw diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean deleted file mode 100644 index 6252f52..0000000 --- a/Nevanlinna/holomorphic_zero.lean +++ /dev/null @@ -1,358 +0,0 @@ -import Init.Classical -import Mathlib.Analysis.Analytic.Meromorphic -import Mathlib.Topology.ContinuousOn -import Mathlib.Analysis.Analytic.IsolatedZeros -import Nevanlinna.holomorphic -import Nevanlinna.analyticOnNhd_zeroSet - - -noncomputable def zeroDivisor - (f : ℂ → ℂ) : - ℂ → ℕ := by - intro z - by_cases hf : AnalyticAt ℂ f z - · exact hf.order.toNat - · exact 0 - - -theorem analyticAtZeroDivisorSupport - {f : ℂ → ℂ} - {z : ℂ} - (h : z ∈ Function.support (zeroDivisor f)) : - AnalyticAt ℂ f z := by - - by_contra h₁f - simp at h - dsimp [zeroDivisor] at h - simp [h₁f] at h - - -theorem zeroDivisor_eq_ord_AtZeroDivisorSupport - {f : ℂ → ℂ} - {z : ℂ} - (h : z ∈ Function.support (zeroDivisor f)) : - zeroDivisor f z = (analyticAtZeroDivisorSupport h).order.toNat := by - - unfold zeroDivisor - simp [analyticAtZeroDivisorSupport h] - - -theorem zeroDivisor_eq_ord_AtZeroDivisorSupport' - {f : ℂ → ℂ} - {z : ℂ} - (h : z ∈ Function.support (zeroDivisor f)) : - zeroDivisor f z = (analyticAtZeroDivisorSupport h).order := by - - unfold zeroDivisor - simp [analyticAtZeroDivisorSupport h] - sorry - - -lemma toNatEqSelf_iff {n : ℕ∞} : n.toNat = n ↔ ∃ m : ℕ, m = n := by - constructor - · intro H₁ - rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists] - by_contra H₂ - rw [H₂] at H₁ - simp at H₁ - · intro H - obtain ⟨m, hm⟩ := H - rw [← hm] - simp - - -lemma natural_if_toNatNeZero {n : ℕ∞} : n.toNat ≠ 0 → ∃ m : ℕ, m = n := by - rw [← ENat.some_eq_coe, ← WithTop.ne_top_iff_exists] - contrapose; simp; tauto - - -theorem zeroDivisor_localDescription - {f : ℂ → ℂ} - {z₀ : ℂ} - (h : z₀ ∈ Function.support (zeroDivisor f)) : - ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by - - have A : zeroDivisor f ↑z₀ ≠ 0 := by exact h - let B := zeroDivisor_eq_ord_AtZeroDivisorSupport h - rw [B] at A - have C := natural_if_toNatNeZero A - obtain ⟨m, hm⟩ := C - have h₂m : m ≠ 0 := by - rw [← hm] at A - simp at A - assumption - rw [eq_comm] at hm - let E := AnalyticAt.order_eq_nat_iff (analyticAtZeroDivisorSupport h) m - let F := hm - rw [E] at F - - have : m = zeroDivisor f z₀ := by - rw [B, hm] - simp - rwa [this] at F - - -theorem zeroDivisor_zeroSet - {f : ℂ → ℂ} - {z₀ : ℂ} - (h : z₀ ∈ Function.support (zeroDivisor f)) : - f z₀ = 0 := by - obtain ⟨g, _, _, h₃⟩ := zeroDivisor_localDescription h - rw [Filter.Eventually.self_of_nhds h₃] - simp - left - exact h - - -theorem zeroDivisor_support_iff - {f : ℂ → ℂ} - {z₀ : ℂ} : - z₀ ∈ Function.support (zeroDivisor f) ↔ - f z₀ = 0 ∧ - AnalyticAt ℂ f z₀ ∧ - ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (zeroDivisor f z₀) • g z := by - constructor - · intro hz - constructor - · exact zeroDivisor_zeroSet hz - · constructor - · exact analyticAtZeroDivisorSupport hz - · exact zeroDivisor_localDescription hz - · intro ⟨h₁, h₂, h₃⟩ - have : zeroDivisor f z₀ = (h₂.order).toNat := by - unfold zeroDivisor - simp [h₂] - simp [this] - simp [(h₂.order_eq_nat_iff (zeroDivisor f z₀)).2 h₃] - obtain ⟨g, h₁g, h₂g, h₃g⟩ := h₃ - rw [Filter.Eventually.self_of_nhds h₃g] at h₁ - simp [h₂g] at h₁ - assumption - - -theorem topOnPreconnected - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ z ∈ U, f z ≠ 0) : - ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by - - by_contra H - push_neg at H - obtain ⟨z', hz'⟩ := H - rw [AnalyticAt.order_eq_top_iff] at hz' - rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz' - have A := AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz' - tauto - - -theorem supportZeroSet - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ z ∈ U, f z ≠ 0) : - U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by - - ext x - constructor - · intro hx - constructor - · exact hx.1 - exact zeroDivisor_zeroSet hx.2 - · simp - intro h₁x h₂x - constructor - · exact h₁x - · let A := zeroDivisor_support_iff (f := f) (z₀ := x) - simp at A - rw [A] - constructor - · exact h₂x - · constructor - · exact h₁f x h₁x - · have B := AnalyticAt.order_eq_nat_iff (h₁f x h₁x) (zeroDivisor f x) - simp at B - rw [← B] - dsimp [zeroDivisor] - simp [h₁f x h₁x] - refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a) - exact topOnPreconnected hU h₁f h₂f h₁x - -/- -theorem discreteZeros - {f : ℂ → ℂ} : - DiscreteTopology (Function.support (zeroDivisor f)) := by - - simp_rw [← singletons_open_iff_discrete, Metric.isOpen_singleton_iff] - intro z - - have A : zeroDivisor f ↑z ≠ 0 := by exact z.2 - let B := zeroDivisor_eq_ord_AtZeroDivisorSupport z.2 - rw [B] at A - have C := natural_if_toNatNeZero A - obtain ⟨m, hm⟩ := C - have h₂m : m ≠ 0 := by - rw [← hm] at A - simp at A - assumption - rw [eq_comm] at hm - let E := AnalyticAt.order_eq_nat_iff (analyticAtZeroDivisorSupport z.2) m - rw [E] at hm - - obtain ⟨g, h₁g, h₂g, h₃g⟩ := hm - - rw [Metric.eventually_nhds_iff_ball] at h₃g - have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by - have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g - have : {0}ᶜ ∈ nhds (g z) := by - exact compl_singleton_mem_nhds_iff.mpr h₂g - - let F := h₄g.preimage_mem_nhds this - rw [Metric.mem_nhds_iff] at F - obtain ⟨ε, h₁ε, h₂ε⟩ := F - use ε - constructor; exact h₁ε - intro y hy - let G := h₂ε hy - simp at G - exact G - obtain ⟨ε₁, h₁ε₁⟩ := this - - obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g - use min ε₁ ε₂ - constructor - · have : 0 < min ε₁ ε₂ := by - rw [lt_min_iff] - exact And.imp_right (fun _ => h₁ε₂) h₁ε₁ - exact this - - intro y - intro h₁y - - have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ - - have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ - - let F := h₂ε₂ y.1 h₂y - rw [zeroDivisor_zeroSet y.2] at F - simp at F - - simp [h₂m] at F - - have : g y.1 ≠ 0 := by - exact h₁ε₁.2 y h₃y - simp [this] at F - ext - rwa [sub_eq_zero] at F --/ - -theorem zeroDivisor_finiteOnCompact - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed! - (h₂U : IsCompact U) : - Set.Finite (U ∩ Function.support (zeroDivisor f)) := by - - have hinter : IsCompact (U ∩ Function.support (zeroDivisor f)) := by - apply IsCompact.of_isClosed_subset h₂U - rw [supportZeroSet] - apply h₁f.continuousOn.preimage_isClosed_of_isClosed - exact IsCompact.isClosed h₂U - exact isClosed_singleton - assumption - assumption - assumption - exact Set.inter_subset_left - - apply hinter.finite - apply DiscreteTopology.of_subset (s := Function.support (zeroDivisor f)) - exact discreteZeros (f := f) - exact Set.inter_subset_right - - - - -noncomputable def zeroDivisorDegree - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) -- not needed! - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed! - ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card - - -lemma zeroDivisorDegreeZero - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) -- not needed! - (h₂U : IsCompact U) - (h₁f : AnalyticOnNhd ℂ f U) - (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed! - 0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by - sorry - - -lemma eliminatingZeros₀ - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) : - ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOnNhd ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) → - (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) → - ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by - - intro n - induction' n with n ih - -- case zero - intro f h₁f h₂f h₃f - use f - rw [zeroDivisorDegreeZero] at h₃f - rw [h₃f] - simpa - - -- case succ - intro f h₁f h₂f h₃f - - let Supp := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset - - have : Supp.Nonempty := by - rw [← Finset.one_le_card] - calc 1 - _ ≤ n + 1 := by exact Nat.le_add_left 1 n - _ = zeroDivisorDegree h₁U h₂U h₁f h₂f := by exact h₃f - _ = Supp.card := by rfl - obtain ⟨z₀, hz₀⟩ := this - dsimp [Supp] at hz₀ - simp only [Set.Finite.mem_toFinset, Set.mem_inter_iff] at hz₀ - - - - - let A := AnalyticOnNhd.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀) - let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2 - let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2 - rw [eq_comm] at B - let C := A B - obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := C - - have h₄g₀ : ∃ z ∈ U, g₀ z ≠ 0 := by sorry - have h₅g₀ : n = zeroDivisorDegree h₁U h₂U h₁g₀ h₄g₀ := by sorry - - obtain ⟨F, h₁F, h₂F⟩ := ih g₀ h₁g₀ h₄g₀ h₅g₀ - use F - constructor - · assumption - · - sorry diff --git a/Nevanlinna/junk/holomorphic_JensenFormula.lean b/Nevanlinna/junk/holomorphic_JensenFormula.lean deleted file mode 100644 index 63e02a7..0000000 --- a/Nevanlinna/junk/holomorphic_JensenFormula.lean +++ /dev/null @@ -1,449 +0,0 @@ -import Mathlib.Analysis.Complex.CauchyIntegral -import Mathlib.Analysis.Analytic.IsolatedZeros -import Nevanlinna.analyticOnNhd_zeroSet -import Nevanlinna.harmonicAt_examples -import Nevanlinna.harmonicAt_meanValue -import Nevanlinna.specialFunctions_CircleIntegral_affine - -open Real - - - -theorem jensen_case_R_eq_one - (f : ℂ → ℂ) - (h₁f : AnalyticOnNhd ℂ 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 - - have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := - (convex_closedBall (0 : ℂ) 1).isPreconnected - - have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := - isCompact_closedBall 0 1 - - have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by - use 0; simp; exact h₂f - - obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f - - have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by - intro z h₁z - apply AnalyticAt.holomorphicAt - exact h₁F z h₁z - - let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log ‖z - s‖ - - have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by - intro z h₁z h₂z - - conv => - left - arg 1 - rw [h₃F] - rw [smul_eq_mul] - rw [norm_mul] - rw [norm_prod] - left - arg 2 - intro b - rw [norm_pow] - simp only [Complex.norm_eq_abs, Finset.univ_eq_attach] - rw [Real.log_mul] - rw [Real.log_prod] - conv => - left - left - arg 2 - intro s - rw [Real.log_pow] - dsimp [G] - abel - - -- ∀ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 - have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by - intro s hs - simp at hs - simp - intro h₂s - rw [h₂s] at h₂z - tauto - exact this - - -- ∏ x ∈ ⋯.toFinset, Complex.abs (z - ↑x) ^ (h'₁f.order x).toNat ≠ 0 - have : ∀ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, Complex.abs (z - ↑x) ^ (h₁f.order x).toNat ≠ 0 := by - intro s hs - simp at hs - simp - intro h₂s - rw [h₂s] at h₂z - tauto - rw [Finset.prod_ne_zero_iff] - exact this - - -- Complex.abs (F z) ≠ 0 - simp - exact h₂F z h₁z - - - have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by - - rw [intervalIntegral.integral_congr_ae] - rw [MeasureTheory.ae_iff] - apply Set.Countable.measure_zero - simp - - have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)} - ⊆ (circleMap 0 1)⁻¹' (Metric.closedBall 0 1 ∩ f⁻¹' {0}) := by - intro a ha - simp at ha - simp - by_contra C - have : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := - circleMap_mem_closedBall 0 (zero_le_one' ℝ) a - exact ha.2 (decompose_f (circleMap 0 1 a) this C) - - apply Set.Countable.mono t₀ - apply Set.Countable.preimage_circleMap - apply Set.Finite.countable - let A := finiteZeros h₁U h₂U h₁f h'₂f - - have : (Metric.closedBall 0 1 ∩ f ⁻¹' {0}) = (Metric.closedBall 0 1).restrict f ⁻¹' {0} := by - ext z - simp - tauto - rw [this] - exact Set.Finite.image Subtype.val A - exact Ne.symm (zero_ne_one' ℝ) - - - have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) - = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) - + ∑ x ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order x).toNat * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by - dsimp [G] - rw [intervalIntegral.integral_add] - rw [intervalIntegral.integral_finset_sum] - simp_rw [intervalIntegral.integral_const_mul] - - -- ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, - -- IntervalIntegrable (fun x => (h'₁f.order i).toNat * - -- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) - intro i _ - apply IntervalIntegrable.const_mul - --simp at this - by_cases h₂i : ‖i.1‖ = 1 - -- case pos - exact int'₂ h₂i - -- case neg - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - - by_contra ha' - conv at h₂i => - arg 1 - rw [← ha'] - rw [Complex.norm_eq_abs] - rw [abs_circleMap_zero 1 x] - simp - tauto - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop - -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π) - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp [h₂F] - -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - apply ContinuousAt.comp - apply DifferentiableAt.continuousAt (𝕜 := ℂ ) - apply HolomorphicAt.differentiableAt - simp [h'₁F] - -- ContinuousAt (fun x => circleMap 0 1 x) x - apply Continuous.continuousAt - apply continuous_circleMap - - have : (fun x => ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) - = ∑ s ∈ (finiteZeros h₁U h₂U h₁f h'₂f).toFinset, (fun x => (h₁f.order s).toNat * log (Complex.abs (circleMap 0 1 x - ↑s))) := by - funext x - simp - rw [this] - apply IntervalIntegrable.sum - intro i _ - apply IntervalIntegrable.const_mul - --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2 - --simp at this - by_cases h₂i : ‖i.1‖ = 1 - -- case pos - exact int'₂ h₂i - -- case neg - --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - - by_contra ha' - conv at h₂i => - arg 1 - rw [← ha'] - rw [Complex.norm_eq_abs] - rw [abs_circleMap_zero 1 x] - simp - tauto - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop - - have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by - let logAbsF := fun w ↦ Real.log ‖F w‖ - have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by - intro z hz - apply logabs_of_holomorphicAt_is_harmonic - apply h'₁F z hz - exact h₂F z hz - - apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀ - - simp_rw [← Complex.norm_eq_abs] at decompose_int_G - rw [t₁] at decompose_int_G - - conv at decompose_int_G => - right - right - arg 2 - intro x - right - rw [int₃ x.2] - simp at decompose_int_G - - rw [int_logAbs_f_eq_int_G] - rw [decompose_int_G] - rw [h₃F] - simp - have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by - calc π⁻¹ * 2⁻¹ * (2 * π * l) - _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring - _ = π⁻¹ * π * l := by ring - _ = (π⁻¹ * π) * l := by ring - _ = 1 * l := by - rw [inv_mul_cancel₀] - exact pi_ne_zero - _ = l := by simp - rw [this] - rw [log_mul] - rw [log_prod] - simp - - rw [finsum_eq_sum_of_support_subset _ (s := (finiteZeros h₁U h₂U h₁f h'₂f).toFinset)] - simp - simp - intro x ⟨h₁x, _⟩ - simp - - dsimp [AnalyticOnNhd.order] at h₁x - simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x - exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x - - -- - intro x hx - simp at hx - simp - intro h₁x - nth_rw 1 [← h₁x] at h₂f - tauto - - -- - rw [Finset.prod_ne_zero_iff] - intro x hx - simp at hx - simp - intro h₁x - nth_rw 1 [← h₁x] at h₂f - tauto - - -- - 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 : AnalyticOnNhd ℂ 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 ℓ : ℂ ≃L[ℂ] ℂ := - { - toFun := fun x ↦ R * x - map_add' := fun x y => DistribSMul.smul_add R x y - map_smul' := fun m x => mul_smul_comm m (↑R) x - invFun := fun x ↦ R⁻¹ * x - left_inv := by - intro x - simp - rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one] - simp - exact ne_of_gt hR - right_inv := by - intro x - simp - rw [← mul_assoc, mul_inv_cancel₀, one_mul] - simp - exact ne_of_gt hR - continuous_toFun := continuous_const_smul R - continuous_invFun := continuous_const_smul R⁻¹ - } - - - let F := f ∘ ℓ - - have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by - apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R) - exact h₁f - intro x _ - apply ℓ.toContinuousLinearMap.analyticAt x - - intro x hx - have : ℓ x = R * x := by rfl - rw [this] - simp - simp at hx - rw [abs_of_pos hR] - calc R * Complex.abs x - _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx - _ = R := by simp - - have h₂F : F 0 ≠ 0 := by - dsimp [F] - have : ℓ 0 = R * 0 := by rfl - rw [this] - 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 - simp_rw [this] at A - simp at A - simp - rw [A] - 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 - 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 - - dsimp [AnalyticOnNhd.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) diff --git a/Nevanlinna/junk/holomorphic_primitive.lean b/Nevanlinna/junk/holomorphic_primitive.lean deleted file mode 100644 index 9b393cc..0000000 --- a/Nevanlinna/junk/holomorphic_primitive.lean +++ /dev/null @@ -1,666 +0,0 @@ -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.SpecialFunctions.Integrals -import Mathlib.MeasureTheory.Integral.DivergenceTheorem -import Mathlib.MeasureTheory.Integral.IntervalIntegral -import Mathlib.MeasureTheory.Function.LocallyIntegrable -import Nevanlinna.partialDeriv -import Nevanlinna.cauchyRiemann - -/- -noncomputable def partialDeriv - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] : E → (E → F) → (E → F) := - fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v)) - - -theorem partialDeriv_compContLinAt - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] - {f : E → F} - {l : F →L[ℝ] G} - {v : E} - {x : E} - (h : DifferentiableAt ℝ f x) : - (partialDeriv v (l ∘ f)) x = (l ∘ partialDeriv v f) x:= by - unfold partialDeriv - rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h] - simp - - -theorem partialDeriv_compCLE - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] - {f : E → F} - {l : F ≃L[ℝ] G} {v : E} : partialDeriv v (l ∘ f) = l ∘ partialDeriv v f := by - funext x - by_cases hyp : DifferentiableAt ℝ f x - · let lCLM : F →L[ℝ] G := l - suffices shyp : partialDeriv v (lCLM ∘ f) x = (lCLM ∘ partialDeriv v f) x from by tauto - apply partialDeriv_compContLinAt - exact hyp - · unfold partialDeriv - rw [fderiv_zero_of_not_differentiableAt] - simp - rw [fderiv_zero_of_not_differentiableAt] - simp - exact hyp - rw [ContinuousLinearEquiv.comp_differentiableAt_iff] - exact hyp - -theorem partialDeriv_smul'₂ - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {f : E → F} {a : ℂ} {v : E} : - partialDeriv v (a • f) = a • partialDeriv v f := by - - funext w - by_cases ha : a = 0 - · unfold partialDeriv - have : a • f = fun y ↦ a • f y := by rfl - rw [this, ha] - simp - · -- Now a is not zero. We present scalar multiplication with a as a continuous linear equivalence. - let smulCLM : F ≃L[ℝ] F := - { - toFun := fun x ↦ a • x - map_add' := fun x y => DistribSMul.smul_add a x y - map_smul' := fun m x => (smul_comm ((RingHom.id ℝ) m) a x).symm - invFun := fun x ↦ a⁻¹ • x - left_inv := by - intro x - simp - rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha, one_smul] - right_inv := by - intro x - simp - rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul] - continuous_toFun := continuous_const_smul a - continuous_invFun := continuous_const_smul a⁻¹ - } - - have : a • f = smulCLM ∘ f := by tauto - rw [this] - rw [partialDeriv_compCLE] - tauto - -theorem CauchyRiemann₄ - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {f : ℂ → F} : - (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by - intro h - unfold partialDeriv - - conv => - left - intro w - rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] - simp - rw [← mul_one Complex.I] - rw [← smul_eq_mul] - conv => - right - right - intro w - rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] - funext w - simp --/ - - -theorem MeasureTheory.integral2_divergence₃ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - (f g : ℝ × ℝ → E) - (h₁f : ContDiff ℝ 1 f) - (h₁g : ContDiff ℝ 1 g) - (a₁ : ℝ) - (a₂ : ℝ) - (b₁ : ℝ) - (b₂ : ℝ) : - ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) (x, y)) (1, 0) + ((fderiv ℝ g) (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y) := by - - apply integral2_divergence_prod_of_hasFDerivWithinAt_off_countable f g (fderiv ℝ f) (fderiv ℝ g) a₁ a₂ b₁ b₂ ∅ - exact Set.countable_empty - -- ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) - exact h₁f.continuous.continuousOn - -- - exact h₁g.continuous.continuousOn - -- - rw [Set.diff_empty] - intro x _ - exact DifferentiableAt.hasFDerivAt ((h₁f.differentiable le_rfl) x) - -- - rw [Set.diff_empty] - intro y _ - exact DifferentiableAt.hasFDerivAt ((h₁g.differentiable le_rfl) y) - -- - apply ContinuousOn.integrableOn_compact - apply IsCompact.prod - exact isCompact_uIcc - exact isCompact_uIcc - apply ContinuousOn.add - apply Continuous.continuousOn - exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁f le_rfl) continuous_const - apply Continuous.continuousOn - exact Continuous.clm_apply (ContDiff.continuous_fderiv h₁g le_rfl) continuous_const - - -theorem integral_divergence₄ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] - (f g : ℂ → E) - (h₁f : ContDiff ℝ 1 f) - (h₁g : ContDiff ℝ 1 g) - (a₁ : ℝ) - (a₂ : ℝ) - (b₁ : ℝ) - (b₂ : ℝ) : - ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, ((fderiv ℝ f) ⟨x, y⟩ ) 1 + ((fderiv ℝ g) ⟨x, y⟩) Complex.I = (((∫ (x : ℝ) in a₁..b₁, g ⟨x, b₂⟩) - ∫ (x : ℝ) in a₁..b₁, g ⟨x, a₂⟩) + ∫ (y : ℝ) in a₂..b₂, f ⟨b₁, y⟩) - ∫ (y : ℝ) in a₂..b₂, f ⟨a₁, y⟩ := by - - let fr : ℝ × ℝ → E := f ∘ Complex.equivRealProdCLM.symm - let gr : ℝ × ℝ → E := g ∘ Complex.equivRealProdCLM.symm - - have sfr {x y : ℝ} : f { re := x, im := y } = fr (x, y) := by exact rfl - have sgr {x y : ℝ} : g { re := x, im := y } = gr (x, y) := by exact rfl - repeat (conv in f { re := _, im := _ } => rw [sfr]) - repeat (conv in g { re := _, im := _ } => rw [sgr]) - - have sfr' {x y : ℝ} {z : ℂ} : (fderiv ℝ f { re := x, im := y }) z = fderiv ℝ fr (x, y) (Complex.equivRealProdCLM z) := by - rw [fderiv.comp] - rw [Complex.equivRealProdCLM.symm.fderiv] - tauto - apply Differentiable.differentiableAt - exact h₁f.differentiable le_rfl - exact Complex.equivRealProdCLM.symm.differentiableAt - conv in ⇑(fderiv ℝ f { re := _, im := _ }) _ => rw [sfr'] - - have sgr' {x y : ℝ} {z : ℂ} : (fderiv ℝ g { re := x, im := y }) z = fderiv ℝ gr (x, y) (Complex.equivRealProdCLM z) := by - rw [fderiv.comp] - rw [Complex.equivRealProdCLM.symm.fderiv] - tauto - apply Differentiable.differentiableAt - exact h₁g.differentiable le_rfl - exact Complex.equivRealProdCLM.symm.differentiableAt - conv in ⇑(fderiv ℝ g { re := _, im := _ }) _ => rw [sgr'] - - apply MeasureTheory.integral2_divergence₃ fr gr _ _ a₁ a₂ b₁ b₂ - -- ContDiff ℝ 1 fr - exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁f - -- ContDiff ℝ 1 gr - exact (ContinuousLinearEquiv.contDiff_comp_iff (ContinuousLinearEquiv.symm Complex.equivRealProdCLM)).mpr h₁g - - -theorem integral_divergence₅ - {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] - (F : ℂ → E) - (hF : Differentiable ℂ F) - (lowerLeft upperRight : ℂ) : - (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, lowerLeft.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨upperRight.re, x⟩ = - (∫ (x : ℝ) in lowerLeft.re..upperRight.re, F ⟨x, upperRight.im⟩) + Complex.I • ∫ (x : ℝ) in lowerLeft.im..upperRight.im, F ⟨lowerLeft.re, x⟩ := by - - let h₁f : ContDiff ℝ 1 F := (hF.contDiff : ContDiff ℂ 1 F).restrict_scalars ℝ - - let h₁g : ContDiff ℝ 1 (-Complex.I • F) := by - have : -Complex.I • F = fun x ↦ -Complex.I • F x := by rfl - rw [this] - apply ContDiff.comp - exact contDiff_const_smul _ - exact h₁f - - let A := integral_divergence₄ (-Complex.I • F) F h₁g h₁f lowerLeft.re upperRight.im upperRight.re lowerLeft.im - have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv ℝ Complex.I F z := by rfl - conv at A in (fderiv ℝ F _) _ => rw [this] - have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv ℝ 1 (-Complex.I • F) z := by rfl - conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this] - conv at A => - left - arg 1 - intro x - arg 1 - intro y - rw [CauchyRiemann₄ hF] - rw [partialDeriv_smul'₂] - simp - simp at A - - have {t₁ t₂ t₃ t₄ : E} : 0 = (t₁ - t₂) + t₃ + t₄ → t₁ + t₃ = t₂ - t₄ := by - intro hyp - calc - t₁ + t₃ = t₁ + t₃ - 0 := by rw [sub_zero (t₁ + t₃)] - _ = t₁ + t₃ - (t₁ - t₂ + t₃ + t₄) := by rw [hyp] - _ = t₂ - t₄ := by abel - let B := this A - repeat - rw [intervalIntegral.integral_symm lowerLeft.im upperRight.im] at B - simp at B - exact B - - -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₁ : ℂ) : - primitive z₀ f = fun z ↦ (primitive z₁ f) z + (primitive z₀ f z₁) := 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 - - let A := integral_divergence₅ f hf ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ - simp at A - - have {a b c d : E} : (b + a) + (c + d) = (a + c) + (b + d) := by - abel - rw [this] - rw [A] - 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 - diff --git a/Nevanlinna/junk/laplace2.lean b/Nevanlinna/junk/laplace2.lean deleted file mode 100644 index f9bfe69..0000000 --- a/Nevanlinna/junk/laplace2.lean +++ /dev/null @@ -1,285 +0,0 @@ -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Analysis.InnerProductSpace.Dual -import Mathlib.Analysis.InnerProductSpace.PiL2 ---import Mathlib.Algebra.BigOperators.Basic -import Mathlib.Analysis.Calculus.ContDiff.Bounds -import Mathlib.Analysis.Calculus.FDeriv.Symmetric ---import Mathlib.LinearAlgebra.Basis ---import Mathlib.LinearAlgebra.Contraction - -open BigOperators -open Finset - - -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] - -noncomputable def realInnerAsElementOfDualTensorprod - {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] - : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner - - -instance - {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] - : NormedAddCommGroup (TensorProduct ℝ E E) where - norm := by - - sorry - dist_self := by - - sorry - - sorry - -/- -instance - {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] - : InnerProductSpace ℝ (TensorProduct ℝ E E) where - smul := _ - one_smul := _ - mul_smul := _ - smul_zero := _ - smul_add := _ - add_smul := _ - zero_smul := _ - norm_smul_le := _ - inner := _ - norm_sq_eq_inner := _ - conj_symm := _ - add_left := _ - smul_left := _ - -/ - - - -noncomputable def dual' - {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] - : (TensorProduct ℝ E E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] TensorProduct ℝ E E := by - - let d := InnerProductSpace.toDual ℝ E - - - let e := d.toLinearEquiv - - let a := TensorProduct.congr e e - - let b := homTensorHomEquiv ℝ E E ℝ ℝ - - sorry - - -variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] -variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] - - -theorem InvariantTensor - [Fintype ι] - (v : Basis ι ℝ E) - (c : ι → ℝ) - (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) : - L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by - - rw [L.map_sum] - simp_rw [L.map_smul_univ] - sorry - - - -theorem BilinearCalc - [Fintype ι] - (v : Basis ι ℝ E) - (c : ι → ℝ) - (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) : - L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by - - rw [L.map_sum] - simp_rw [L.map_smul_univ] - sorry - -/- -lemma c2 - [Fintype ι] - (b : Basis ι ℝ E) - (hb : Orthonormal ℝ b) - (x y : E) : - ⟪x, y⟫_ℝ = ∑ i : ι, ⟪x, b i⟫_ℝ * ⟪y, b i⟫_ℝ := by - rw [vectorPresentation b hb x] - rw [vectorPresentation b hb y] - rw [Orthonormal.inner_sum hb] - simp - conv => - right - arg 2 - intro i' - rw [Orthonormal.inner_left_fintype hb] - rw [Orthonormal.inner_left_fintype hb] --/ - -lemma fin_sum - [Fintype ι] - (f : ι → ι → F) : - ∑ r : Fin 2 → ι, f (r 0) (r 1) = ∑ r₀ : ι, (∑ r₁ : ι, f r₀ r₁) := by - - rw [← Fintype.sum_prod_type'] - apply Fintype.sum_equiv (finTwoArrowEquiv ι) - intro x - dsimp - - -theorem LaplaceIndep - [Fintype ι] [DecidableEq ι] - (v₁ : OrthonormalBasis ι ℝ E) - (v₂ : OrthonormalBasis ι ℝ E) - (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) : - ∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by - - have vector_vs_function - {y : Fin 2 → ι} - {v : ι → E} - : (fun i => v (y i)) = ![v (y 0), v (y 1)] := by - funext i - by_cases h : i = 0 - · rw [h] - simp - · rw [Fin.eq_one_of_neq_zero i h] - simp - - conv => - right - arg 2 - intro i - rw [v₁.sum_repr' (v₂ i)] - rw [BilinearCalc] - rw [Finset.sum_comm] - conv => - right - arg 2 - intro y - rw [← Finset.sum_smul] - rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))] - rw [vector_vs_function] - simp - - rw [fin_sum (fun i₀ ↦ (fun i₁ ↦ ⟪v₁ i₀, v₁ i₁⟫_ℝ • L ![v₁ i₀, v₁ i₁]))] - - have xx {r₀ : ι} : ∀ r₁ : ι, r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • L ![v₁ r₀, v₁ r₁] = 0 := by - intro r₁ hr₁ - rw [orthonormal_iff_ite.1 hv₁] - simp - tauto - - conv => - right - arg 2 - intro r₀ - rw [Fintype.sum_eq_single r₀ xx] - rw [orthonormal_iff_ite.1 hv₁] - apply sum_congr - rfl - intro x _ - rw [vector_vs_function] - simp - - -noncomputable def Laplace_wrt_basis - [Fintype ι] - (v : Basis ι ℝ E) - (_ : Orthonormal ℝ v) - (f : E → F) : - E → F := - fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i] - - -theorem LaplaceIndep' - [Fintype ι] [DecidableEq ι] - (v₁ : OrthonormalBasis ι ℝ E) - (v₂ : OrthonormalBasis ι ℝ E) - (f : E → F) - : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by - - funext z - unfold Laplace_wrt_basis - let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv ℝ 2 f z) - have vector_vs_function - {v : E} - : ![v, v] = (fun _ => v) := by - funext i - by_cases h : i = 0 - · rw [h] - simp - · rw [Fin.eq_one_of_neq_zero i h] - simp - conv => - left - arg 2 - intro i - rw [vector_vs_function] - conv => - right - arg 2 - intro i - rw [vector_vs_function] - assumption - - -theorem LaplaceIndep'' - [Fintype ι₁] [DecidableEq ι₁] - (v₁ : Basis ι₁ ℝ E) - (hv₁ : Orthonormal ℝ v₁) - [Fintype ι₂] [DecidableEq ι₂] - (v₂ : Basis ι₂ ℝ E) - (hv₂ : Orthonormal ℝ v₂) - (f : E → F) - : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by - - have b : ι₁ ≃ ι₂ := by - apply Fintype.equivOfCardEq - rw [← FiniteDimensional.finrank_eq_card_basis v₁] - rw [← FiniteDimensional.finrank_eq_card_basis v₂] - - let v'₁ := Basis.reindex v₁ b - have hv'₁ : Orthonormal ℝ v'₁ := by - let A := Basis.reindex_apply v₁ b - have : ⇑v'₁ = v₁ ∘ b.symm := by - funext i - exact A i - rw [this] - let B := Orthonormal.comp hv₁ b.symm - apply B - exact Equiv.injective b.symm - rw [← LaplaceIndep' v'₁ hv'₁ v₂ hv₂ f] - - unfold Laplace_wrt_basis - simp - funext z - - rw [← Equiv.sum_comp b.symm] - apply Fintype.sum_congr - intro i₂ - congr - rw [Basis.reindex_apply v₁ b i₂] - - -noncomputable def Laplace - (f : E → F) - : E → F := by - exact Laplace_wrt_basis (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal f - - -theorem LaplaceIndep''' - [Fintype ι] [DecidableEq ι] - (v : Basis ι ℝ E) - (hv : Orthonormal ℝ v) - (f : E → F) - : (Laplace f) = (Laplace_wrt_basis v hv f) := by - - unfold Laplace - apply LaplaceIndep'' (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal v hv f - - -theorem Complex.Laplace' - (f : ℂ → F) - : (Laplace f) = fun z ↦ (iteratedFDeriv ℝ 2 f z) ![1, 1] + (iteratedFDeriv ℝ 2 f z) ![Complex.I, Complex.I] := by - - rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f] - unfold Laplace_wrt_basis - simp diff --git a/Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean b/Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean deleted file mode 100644 index 23bb8df..0000000 --- a/Nevanlinna/junk/stronglyMeromorphic_JensenFormula_1.lean +++ /dev/null @@ -1,528 +0,0 @@ -import Mathlib.Analysis.Complex.CauchyIntegral -import Mathlib.Analysis.Analytic.IsolatedZeros -import Nevanlinna.analyticOnNhd_zeroSet -import Nevanlinna.harmonicAt_examples -import Nevanlinna.harmonicAt_meanValue -import Nevanlinna.specialFunctions_CircleIntegral_affine -import Nevanlinna.stronglyMeromorphicOn -import Nevanlinna.stronglyMeromorphicOn_eliminate -import Nevanlinna.meromorphicOn_divisor - -open Real - - - -theorem jensen_case_R_eq_one' - (f : ℂ → ℂ) - (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1)) - (h₂f : f 0 ≠ 0) : - log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by - - have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by - constructor - · apply Metric.nonempty_closedBall.mpr (by simp) - · exact (convex_closedBall (0 : ℂ) 1).isPreconnected - - have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := - isCompact_closedBall 0 1 - - have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by - use ⟨0, Metric.mem_closedBall_self (by simp)⟩ - - have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by - exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor - - have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by - intro x - contrapose - simp - intro hx - rw [hx] - simp - rw [finsum_eq_sum_of_support_subset _ h₄f] - - obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f h'₂f - - have h₁F : Function.mulSupport (fun u ↦ fun z => (z - u) ^ (h₁f.meromorphicOn.divisor u)) ⊆ h₃f.toFinset := by - intro u - contrapose - simp - intro hu - rw [hu] - simp - exact rfl - rw [finprod_eq_prod_of_mulSupport_subset _ h₁F] at h₄F - - let G := fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖ - - have h₁G {z : ℂ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) ⊆ h₃f.toFinset := by - intro s - contrapose - simp - intro hs - rw [hs] - simp - - have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by - intro z h₁z h₂z - - rw [h₄F] - simp only [Pi.mul_apply, norm_mul] - simp only [Finset.prod_apply, norm_prod, norm_zpow] - rw [Real.log_mul] - rw [Real.log_prod] - simp_rw [Real.log_zpow] - dsimp only [G] - rw [finsum_eq_sum_of_support_subset _ h₁G] - -- - intro x hx - have : z ≠ x := by - by_contra hCon - rw [← hCon] at hx - simp at hx - rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z - unfold MeromorphicOn.divisor at hx - simp [h₁z] at hx - tauto - apply zpow_ne_zero - simpa - -- Complex.abs (F z) ≠ 0 - simp - exact h₃F ⟨z, h₁z⟩ - -- - rw [Finset.prod_ne_zero_iff] - intro x hx - have : z ≠ x := by - by_contra hCon - rw [← hCon] at hx - simp at hx - rw [← StronglyMeromorphicAt.order_eq_zero_iff] at h₂z - unfold MeromorphicOn.divisor at hx - simp [h₁z] at hx - tauto - apply zpow_ne_zero - simpa - - - have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by - - rw [intervalIntegral.integral_congr_ae] - rw [MeasureTheory.ae_iff] - apply Set.Countable.measure_zero - simp - - have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)} - ⊆ (circleMap 0 1)⁻¹' (h₃f.toFinset) := by - intro a ha - simp at ha - simp - by_contra C - have t₀ : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 := - circleMap_mem_closedBall 0 (zero_le_one' ℝ) a - have t₁ : f (circleMap 0 1 a) ≠ 0 := by - let A := h₁f (circleMap 0 1 a) t₀ - rw [← A.order_eq_zero_iff] - unfold MeromorphicOn.divisor at C - simp [t₀] at C - rcases C with C₁|C₂ - · assumption - · let B := h₁f.meromorphicOn.order_ne_top' h₁U - let C := fun q ↦ B q ⟨(circleMap 0 1 a), t₀⟩ - rw [C₂] at C - have : ∃ u : (Metric.closedBall (0 : ℂ) 1), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by - use ⟨(0 : ℂ), (by simp)⟩ - let H := h₁f 0 (by simp) - let K := H.order_eq_zero_iff.2 h₂f - rw [K] - simp - let D := C this - tauto - exact ha.2 (decompose_f (circleMap 0 1 a) t₀ t₁) - - apply Set.Countable.mono t₀ - apply Set.Countable.preimage_circleMap - apply Set.Finite.countable - exact Finset.finite_toSet h₃f.toFinset - -- - simp - - - have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) - = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x)))) - + ∑ᶠ x, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by - dsimp [G] - - rw [intervalIntegral.integral_add] - congr - have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) ⊆ h₃f.toFinset := by - intro s hs - simp at hs - simp [hs.1] - conv => - left - arg 1 - intro x - rw [finsum_eq_sum_of_support_subset _ t₀] - rw [intervalIntegral.integral_finset_sum] - let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x)) - have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))) ⊆ h₃f.toFinset := by - simp - intro s - contrapose! - simp - tauto - conv => - right - rw [finsum_eq_sum_of_support_subset _ t₁] - simp - - -- ∀ i ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, - -- IntervalIntegrable (fun x => (h'₁f.order i).toNat * - -- log (Complex.abs (circleMap 0 1 x - ↑i))) MeasureTheory.volume 0 (2 * π) - intro i _ - apply IntervalIntegrable.const_mul - --simp at this - by_cases h₂i : ‖i‖ = 1 - -- case pos - exact int'₂ h₂i - -- case neg - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - - by_contra ha' - conv at h₂i => - arg 1 - rw [← ha'] - rw [Complex.norm_eq_abs] - rw [abs_circleMap_zero 1 x] - simp - tauto - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop - -- IntervalIntegrable (fun x => log (Complex.abs (F (circleMap 0 1 x)))) MeasureTheory.volume 0 (2 * π) - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - exact h₃F ⟨(circleMap 0 1 x), (by simp)⟩ - - -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - apply ContinuousAt.comp - apply DifferentiableAt.continuousAt (𝕜 := ℂ) - apply AnalyticAt.differentiableAt - exact h₂F (circleMap 0 1 x) (by simp) - -- ContinuousAt (fun x => circleMap 0 1 x) x - apply Continuous.continuousAt - apply continuous_circleMap - -- IntervalIntegrable (fun x => ∑ᶠ (s : ℂ), ↑(↑⋯.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) MeasureTheory.volume 0 (2 * π) - --simp? at h₁G - have h₁G' {z : ℂ} : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * log (Complex.abs (z - s))) ⊆ ↑h₃f.toFinset := by - exact h₁G - conv => - arg 1 - intro z - rw [finsum_eq_sum_of_support_subset _ h₁G'] - conv => - arg 1 - rw [← Finset.sum_fn] - apply IntervalIntegrable.sum - intro i _ - apply IntervalIntegrable.const_mul - --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2 - --simp at this - by_cases h₂i : ‖i‖ = 1 - -- case pos - exact int'₂ h₂i - -- case neg - --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry - apply Continuous.intervalIntegrable - apply continuous_iff_continuousAt.2 - intro x - have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) := - rfl - rw [this] - apply ContinuousAt.comp - apply Real.continuousAt_log - simp - - by_contra ha' - conv at h₂i => - arg 1 - rw [← ha'] - rw [Complex.norm_eq_abs] - rw [abs_circleMap_zero 1 x] - simp - tauto - apply ContinuousAt.comp - apply Complex.continuous_abs.continuousAt - fun_prop - - have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by - let logAbsF := fun w ↦ Real.log ‖F w‖ - have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by - intro z hz - apply logabs_of_holomorphicAt_is_harmonic - exact AnalyticAt.holomorphicAt (h₂F z hz) - exact h₃F ⟨z, hz⟩ - - apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀ - - simp_rw [← Complex.norm_eq_abs] at decompose_int_G - rw [t₁] at decompose_int_G - - - have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖) ⊆ ↑h₃f.toFinset := by - intro s hs - simp at hs - simp [hs.1] - rw [finsum_eq_sum_of_support_subset _ h₁G'] at decompose_int_G - have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖ = 0 := by - apply Finset.sum_eq_zero - intro x hx - rw [int₃ _] - simp - simp at hx - let ZZ := h₁f.meromorphicOn.divisor.supportInU - simp at ZZ - let UU := ZZ x hx - simpa - rw [this] at decompose_int_G - - - simp at decompose_int_G - - rw [int_logAbs_f_eq_int_G] - rw [decompose_int_G] - let X := h₄F - nth_rw 1 [h₄F] - simp - have {l : ℝ} : π⁻¹ * 2⁻¹ * (2 * π * l) = l := by - calc π⁻¹ * 2⁻¹ * (2 * π * l) - _ = π⁻¹ * (2⁻¹ * 2) * π * l := by ring - _ = π⁻¹ * π * l := by ring - _ = (π⁻¹ * π) * l := by ring - _ = 1 * l := by - rw [inv_mul_cancel₀] - exact pi_ne_zero - _ = l := by simp - rw [this] - rw [log_mul] - rw [log_prod] - simp - rw [add_comm] - -- - intro x hx - simp at hx - rw [zpow_ne_zero_iff] - by_contra hCon - simp at hCon - rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f - rw [hCon] at hx - unfold MeromorphicOn.divisor at hx - simp at hx - rw [h₂f] at hx - tauto - assumption - -- - simp - - by_contra hCon - nth_rw 1 [h₄F] at h₂f - simp at h₂f - tauto - -- - rw [Finset.prod_ne_zero_iff] - intro x hx - simp at hx - rw [zpow_ne_zero_iff] - by_contra hCon - simp at hCon - rw [← (h₁f 0 (by simp)).order_eq_zero_iff] at h₂f - rw [hCon] at hx - unfold MeromorphicOn.divisor at hx - simp at hx - rw [h₂f] at hx - tauto - assumption - - - -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 : StronglyMeromorphicOn f (Metric.closedBall 0 R)) - (h₂f : f 0 ≠ 0) : - log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by - - - let ℓ : ℂ ≃L[ℂ] ℂ := - { - toFun := fun x ↦ R * x - map_add' := fun x y => DistribSMul.smul_add R x y - map_smul' := fun m x => mul_smul_comm m (↑R) x - invFun := fun x ↦ R⁻¹ * x - left_inv := by - intro x - simp - rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one] - simp - exact ne_of_gt hR - right_inv := by - intro x - simp - rw [← mul_assoc, mul_inv_cancel₀, one_mul] - simp - exact ne_of_gt hR - continuous_toFun := continuous_const_smul R - continuous_invFun := continuous_const_smul R⁻¹ - } - - - let F := f ∘ ℓ - - have h₁F : StronglyMeromorphicOn F (Metric.closedBall 0 1) := by - sorry -/- - apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R) - exact h₁f - intro x _ - apply ℓ.toContinuousLinearMap.analyticAt x - - intro x hx - have : ℓ x = R * x := by rfl - rw [this] - simp - simp at hx - rw [abs_of_pos hR] - calc R * Complex.abs x - _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx - _ = R := by simp --/ - have h₂F : F 0 ≠ 0 := by - dsimp [F] - have : ℓ 0 = R * 0 := by rfl - rw [this] - 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 - simp_rw [this] at A - simp at A - simp - rw [A] - 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 - 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 - - dsimp [AnalyticOnNhd.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) diff --git a/Nevanlinna/specialFunctions_Integral_log.lean b/Nevanlinna/specialFunctions_Integral_log.lean deleted file mode 100644 index 9b8eaae..0000000 --- a/Nevanlinna/specialFunctions_Integral_log.lean +++ /dev/null @@ -1,65 +0,0 @@ -import Mathlib.Analysis.SpecialFunctions.Integrals -import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog -import Mathlib.MeasureTheory.Integral.CircleIntegral -import Mathlib.MeasureTheory.Measure.Restrict - -open scoped Interval Topology -open Real Filter MeasureTheory intervalIntegral - --- The following theorem was suggested by Gareth Ma on Zulip - - -theorem logInt - {t : ℝ} - (ht : 0 < t) : - ∫ x in (0 : ℝ)..t, log x = t * log t - t := by - rw [← integral_add_adjacent_intervals (b := 1)] - trans (-1) + (t * log t - t + 1) - · congr - · -- ∫ x in 0..1, log x = -1, same proof as before - rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := -1)] - · simp - · simp - · intro x hx - norm_num at hx - convert (hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x) using 1 - norm_num - · rw [← neg_neg log] - apply IntervalIntegrable.neg - apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) - · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg - · intro x hx - norm_num at hx - convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1 - norm_num - · intro x hx - norm_num at hx - rw [Pi.neg_apply, Left.nonneg_neg_iff] - exact (log_nonpos_iff hx.left).mpr hx.right.le - · have := tendsto_log_mul_rpow_nhds_zero zero_lt_one - simp_rw [rpow_one, mul_comm] at this - -- tendsto_nhdsWithin_of_tendsto_nhds should be under Tendsto namespace - convert this.sub (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) - norm_num - · rw [(by simp : -1 = 1 * log 1 - 1)] - apply tendsto_nhdsWithin_of_tendsto_nhds - exact (continuousAt_id.mul (continuousAt_log one_ne_zero)).sub continuousAt_id - · -- ∫ x in 1..t, log x = t * log t + 1, just use integral_log_of_pos - rw [integral_log_of_pos zero_lt_one ht] - norm_num - · abel - · -- log is integrable on [[0, 1]] - rw [← neg_neg log] - apply IntervalIntegrable.neg - apply intervalIntegrable_deriv_of_nonneg (g := fun x ↦ -(x * log x - x)) - · exact (continuous_mul_log.continuousOn.sub continuous_id.continuousOn).neg - · intro x hx - norm_num at hx - convert ((hasDerivAt_mul_log hx.left.ne.symm).sub (hasDerivAt_id x)).neg using 1 - norm_num - · intro x hx - norm_num at hx - rw [Pi.neg_apply, Left.nonneg_neg_iff] - exact (log_nonpos_iff hx.left).mpr hx.right.le - · -- log is integrable on [[0, t]] - simp [Set.mem_uIcc, ht] diff --git a/lake-manifest.json b/lake-manifest.json index 0720952..53e6c9a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "504007f6f772de93ea967b17320baeac5a21cb55", + "rev": "0571c82877b7c2b508cbc9a39e041eb117d050b7", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,