Compare commits
No commits in common. "main" and "feature/locallyHarmonic" have entirely different histories.
main
...
feature/lo
|
@ -1,238 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Mathlib.Analysis.Complex.Basic
|
||||
import Mathlib.Analysis.Analytic.Linear
|
||||
|
||||
|
||||
theorem AnalyticAt.order_neq_top_iff
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : AnalyticAt ℂ f z₀) :
|
||||
hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
|
||||
rw [← hf.order_eq_nat_iff]
|
||||
constructor
|
||||
· intro h₁f
|
||||
exact Eq.symm (ENat.coe_toNat h₁f)
|
||||
· intro h₁f
|
||||
exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
|
||||
|
||||
|
||||
theorem AnalyticAt.order_mul
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf₁ : AnalyticAt ℂ f₁ z₀)
|
||||
(hf₂ : AnalyticAt ℂ f₂ z₀) :
|
||||
(hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
|
||||
by_cases h₂f₁ : hf₁.order = ⊤
|
||||
· simp [h₂f₁]
|
||||
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
|
||||
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
|
||||
use t
|
||||
constructor
|
||||
· intro y hy
|
||||
rw [h₁t y hy]
|
||||
ring
|
||||
· exact ⟨h₂t, h₃t⟩
|
||||
· by_cases h₂f₂ : hf₂.order = ⊤
|
||||
· simp [h₂f₂]
|
||||
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff]
|
||||
rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂
|
||||
obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
|
||||
use t
|
||||
constructor
|
||||
· intro y hy
|
||||
rw [h₁t y hy]
|
||||
ring
|
||||
· exact ⟨h₂t, h₃t⟩
|
||||
· obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁))
|
||||
obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂))
|
||||
rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add]
|
||||
rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)]
|
||||
use g₁ * g₂
|
||||
constructor
|
||||
· exact AnalyticAt.mul h₁g₁ h₁g₂
|
||||
· constructor
|
||||
· simp; tauto
|
||||
· obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁
|
||||
obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂
|
||||
rw [eventually_nhds_iff]
|
||||
use t₁ ∩ t₂
|
||||
constructor
|
||||
· intro y hy
|
||||
rw [h₁t₁ y hy.1, h₁t₂ y hy.2]
|
||||
simp; ring
|
||||
· constructor
|
||||
· exact IsOpen.inter h₂t₁ h₂t₂
|
||||
· exact Set.mem_inter h₃t₁ h₃t₂
|
||||
|
||||
|
||||
theorem AnalyticAt.order_eq_zero_iff
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : AnalyticAt ℂ f z₀) :
|
||||
hf.order = 0 ↔ f z₀ ≠ 0 := by
|
||||
|
||||
have : (0 : ENat) = (0 : Nat) := by rfl
|
||||
rw [this, AnalyticAt.order_eq_nat_iff hf 0]
|
||||
|
||||
constructor
|
||||
· intro hz
|
||||
obtain ⟨g, _, h₂g, h₃g⟩ := hz
|
||||
simp at h₃g
|
||||
rw [Filter.Eventually.self_of_nhds h₃g]
|
||||
tauto
|
||||
· intro hz
|
||||
use f
|
||||
constructor
|
||||
· exact hf
|
||||
· constructor
|
||||
· exact hz
|
||||
· simp
|
||||
|
||||
|
||||
theorem AnalyticAt.order_pow
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
{n : ℕ}
|
||||
(hf : AnalyticAt ℂ f z₀) :
|
||||
(hf.pow n).order = n * hf.order := by
|
||||
|
||||
induction' n with n hn
|
||||
· simp; rw [AnalyticAt.order_eq_zero_iff]; simp
|
||||
· simp
|
||||
simp_rw [add_mul, pow_add]
|
||||
simp
|
||||
rw [AnalyticAt.order_mul (hf.pow n) hf]
|
||||
rw [hn]
|
||||
|
||||
|
||||
theorem AnalyticAt.supp_order_toNat
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf : AnalyticAt ℂ f z₀) :
|
||||
hf.order.toNat ≠ 0 → f z₀ = 0 := by
|
||||
|
||||
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 hℓ
|
||||
exact h₂t
|
||||
· exact h₃t
|
||||
|
||||
|
||||
theorem AnalyticAt.order_congr
|
||||
{f₁ f₂ : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
(hf₁ : AnalyticAt ℂ f₁ z₀)
|
||||
(hf : f₁ =ᶠ[nhds z₀] f₂) :
|
||||
hf₁.order = (hf₁.congr hf).order := by
|
||||
|
||||
by_cases h₁f₁ : hf₁.order = ⊤
|
||||
rw [h₁f₁, eq_comm, AnalyticAt.order_eq_top_iff]
|
||||
rw [AnalyticAt.order_eq_top_iff] at h₁f₁
|
||||
exact Filter.EventuallyEq.rw h₁f₁ (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
|
||||
--
|
||||
let n := hf₁.order.toNat
|
||||
have hn : hf₁.order = n := Eq.symm (ENat.coe_toNat h₁f₁)
|
||||
rw [hn, eq_comm, 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
|
||||
· assumption
|
||||
· constructor
|
||||
· assumption
|
||||
· exact Filter.EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (id (Filter.EventuallyEq.symm hf))
|
||||
|
||||
|
||||
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
|
||||
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
|
||||
|
||||
have : AnalyticAt ℂ (0 : ℂ → ℂ) z₀ := by
|
||||
apply analyticAt_const
|
||||
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
|
||||
|
||||
have t₁ : AnalyticAt ℂ (fun z => ℓ z - ℓ z₀) z₀ := by
|
||||
apply AnalyticAt.sub
|
||||
exact ContinuousLinearEquiv.analyticAt ℓ z₀
|
||||
exact analyticAt_const
|
||||
have t₀ : AnalyticAt ℂ (fun z => (ℓ z - ℓ z₀) ^ n) z₀ := by
|
||||
exact pow t₁ n
|
||||
have : AnalyticAt ℂ (fun z ↦ (ℓ z - ℓ z₀) ^ n • g (ℓ z) : ℂ → ℂ) z₀ := by
|
||||
apply AnalyticAt.mul
|
||||
exact t₀
|
||||
apply AnalyticAt.comp h₁g
|
||||
exact ContinuousLinearEquiv.analyticAt ℓ z₀
|
||||
rw [AnalyticAt.order_congr (hf.comp (ℓ.analyticAt z₀)) A]
|
||||
simp
|
||||
|
||||
rw [AnalyticAt.order_mul t₀ ((h₁g.comp (ℓ.analyticAt z₀)))]
|
||||
|
||||
have : t₁.order = (1 : ℕ) := by
|
||||
rw [AnalyticAt.order_eq_nat_iff]
|
||||
use (fun _ ↦ ℓ 1)
|
||||
simp
|
||||
constructor
|
||||
· exact analyticAt_const
|
||||
· apply Filter.Eventually.of_forall
|
||||
intro x
|
||||
calc ℓ x - ℓ z₀
|
||||
_ = ℓ (x - z₀) := by
|
||||
exact Eq.symm (ContinuousLinearEquiv.map_sub ℓ x z₀)
|
||||
_ = ℓ ((x - z₀) * 1) := by
|
||||
simp
|
||||
_ = (x - z₀) * ℓ 1 := by
|
||||
rw [← smul_eq_mul, ← smul_eq_mul]
|
||||
exact ContinuousLinearEquiv.map_smul ℓ (x - z₀) 1
|
||||
|
||||
have : t₀.order = n := by
|
||||
rw [AnalyticAt.order_pow t₁, this]
|
||||
simp
|
||||
|
||||
rw [this]
|
||||
|
||||
have : (comp h₁g (ContinuousLinearEquiv.analyticAt ℓ z₀)).order = 0 := by
|
||||
rwa [AnalyticAt.order_eq_zero_iff]
|
||||
rw [this]
|
||||
|
||||
simp
|
|
@ -1,461 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Constructions
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Mathlib.Analysis.Complex.Basic
|
||||
import Nevanlinna.analyticAt
|
||||
|
||||
|
||||
noncomputable def AnalyticOn.order
|
||||
{f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
|
||||
|
||||
|
||||
theorem AnalyticOn.order_eq_nat_iff
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{z₀ : U}
|
||||
(hf : AnalyticOn ℂ f U)
|
||||
(n : ℕ) :
|
||||
hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ 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 [AnalyticOn.order]
|
||||
rw [AnalyticAt.order_eq_nat_iff]
|
||||
use g
|
||||
exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
|
||||
|
||||
|
||||
theorem AnalyticOn.support_of_order₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOn ℂ f U) :
|
||||
Function.support hf.order = U.restrict f⁻¹' {0} := by
|
||||
ext u
|
||||
simp [AnalyticOn.order]
|
||||
rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
|
||||
|
||||
|
||||
theorem AnalyticOn.eliminateZeros
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
{A : Finset U}
|
||||
(hf : AnalyticOn ℂ f U)
|
||||
(n : U → ℕ) :
|
||||
(∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ 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 : ℂ → ℂ), AnalyticOn ℂ 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₁⟩ := (AnalyticOn.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 : AnalyticOn ℂ 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 : AnalyticOn ℂ 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 : AnalyticOn ℂ 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 AnalyticOnCompact.eliminateZeros
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ 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, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.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 AnalyticOnCompact.eliminateZeros₂
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ), AnalyticOn ℂ 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, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.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 AnalyticOnCompact.eliminateZeros₁
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsPreconnected U)
|
||||
(h₂U : IsCompact U)
|
||||
(h₁f : AnalyticOn ℂ f U)
|
||||
(h₂f : ∃ u ∈ U, f u ≠ 0) :
|
||||
∃ (g : ℂ → ℂ), AnalyticOn ℂ 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, AnalyticOn.order]
|
||||
rw [eq_comm]
|
||||
apply XX h₁U
|
||||
exact h₂f
|
||||
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.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
|
|
@ -32,6 +32,17 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.
|
|||
open TensorProduct
|
||||
|
||||
|
||||
lemma OrthonormalBasis.sum_repr'
|
||||
{𝕜 : Type*} [RCLike 𝕜]
|
||||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
|
||||
[Fintype ι]
|
||||
(b : OrthonormalBasis ι 𝕜 E)
|
||||
(v : E) :
|
||||
v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
|
||||
nth_rw 1 [← (b.sum_repr v)]
|
||||
simp_rw [b.repr_apply_apply v]
|
||||
|
||||
|
||||
noncomputable def InnerProductSpace.canonicalContravariantTensor
|
||||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
|
||||
: E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner
|
||||
|
@ -53,7 +64,7 @@ theorem InnerProductSpace.canonicalCovariantTensorRepresentation
|
|||
right
|
||||
arg 2
|
||||
intro i
|
||||
rw [← w.sum_repr' (v i)]
|
||||
rw [w.sum_repr' (v i)]
|
||||
simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
|
||||
|
||||
conv =>
|
||||
|
|
|
@ -58,13 +58,13 @@ theorem CauchyRiemann₄
|
|||
simp
|
||||
rw [← mul_one Complex.I]
|
||||
rw [← smul_eq_mul]
|
||||
rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
|
||||
conv =>
|
||||
right
|
||||
right
|
||||
intro w
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
|
||||
funext w
|
||||
simp
|
||||
|
||||
|
||||
theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {z : ℂ} : (DifferentiableAt ℂ f z)
|
||||
→ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
|
||||
|
@ -77,8 +77,8 @@ theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
|||
simp
|
||||
rw [← mul_one Complex.I]
|
||||
rw [← smul_eq_mul]
|
||||
rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
|
||||
conv =>
|
||||
right
|
||||
right
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||||
simp
|
||||
|
|
|
@ -1,9 +1,9 @@
|
|||
import Nevanlinna.laplace
|
||||
|
||||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||||
variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁]
|
||||
variable {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℂ F₁] [CompleteSpace F₁]
|
||||
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
|
||||
variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁]
|
||||
variable {G₁ : Type*} [NormedAddCommGroup G₁] [NormedSpace ℂ G₁] [CompleteSpace G₁]
|
||||
|
||||
|
||||
def Harmonic (f : ℂ → F) : Prop :=
|
||||
|
@ -33,7 +33,7 @@ theorem HarmonicAt_iff
|
|||
· constructor
|
||||
· exact Set.mem_inter h₂s₁ h₃s₂
|
||||
· constructor
|
||||
· exact h₃s₁.mono Set.inter_subset_left
|
||||
· exact h₃s₁.mono (Set.inter_subset_left s₁ s₂)
|
||||
· intro z hz
|
||||
exact h₂t₂ (h₁s₂ hz.2)
|
||||
· intro hyp
|
||||
|
@ -47,24 +47,6 @@ theorem HarmonicAt_iff
|
|||
· apply (IsOpen.mem_nhds_iff h₁s).2 h₂s
|
||||
· exact h₂f
|
||||
|
||||
theorem HarmonicAt_isOpen
|
||||
(f : ℂ → F) :
|
||||
IsOpen { x : ℂ | HarmonicAt f x } := by
|
||||
|
||||
rw [← subset_interior_iff_isOpen]
|
||||
intro x hx
|
||||
simp at hx
|
||||
obtain ⟨s, h₁s, h₂s, h₃s⟩ := HarmonicAt_iff.1 hx
|
||||
use s
|
||||
constructor
|
||||
· simp
|
||||
constructor
|
||||
· exact h₁s
|
||||
· intro x hx
|
||||
simp
|
||||
rw [HarmonicAt_iff]
|
||||
use s
|
||||
· exact h₂s
|
||||
|
||||
theorem HarmonicAt_eventuallyEq {f₁ f₂ : ℂ → F} {x : ℂ} (h : f₁ =ᶠ[nhds x] f₂) : HarmonicAt f₁ x ↔ HarmonicAt f₂ x := by
|
||||
constructor
|
|
@ -1,139 +0,0 @@
|
|||
import Nevanlinna.analyticAt
|
||||
|
||||
|
||||
structure Divisor where
|
||||
toFun : ℂ → ℤ
|
||||
discreteSupport : DiscreteTopology (Function.support toFun)
|
||||
|
||||
instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
|
||||
coe := Divisor.toFun
|
||||
attribute [coe] Divisor.toFun
|
||||
|
||||
|
||||
|
||||
noncomputable def Divisor.deg
|
||||
(D : Divisor) : ℤ := ∑ᶠ z, D z
|
||||
|
||||
noncomputable def Divisor.n_trunk
|
||||
(D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
|
||||
|
||||
noncomputable def Divisor.n
|
||||
(D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
|
||||
|
||||
noncomputable def Divisor.N_trunk
|
||||
(D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
|
||||
|
||||
theorem Divisor.compactSupport
|
||||
(D : Divisor)
|
||||
{U : Set ℂ}
|
||||
(h₁U : IsCompact U)
|
||||
(h₂U : Function.support D ⊆ U) :
|
||||
Set.Finite (Function.support D) := by
|
||||
sorry
|
||||
|
||||
|
||||
noncomputable def AnalyticOn.zeroDivisor
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOn ℂ f U) :
|
||||
Divisor where
|
||||
|
||||
toFun := by
|
||||
intro z
|
||||
if hz : z ∈ U then
|
||||
exact ((hf z hz).order.toNat : ℤ)
|
||||
else
|
||||
exact 0
|
||||
|
||||
discreteSupport := by
|
||||
simp_rw [← singletons_open_iff_discrete]
|
||||
simp_rw [Metric.isOpen_singleton_iff]
|
||||
simp
|
||||
|
||||
-- simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
|
||||
|
||||
intro a ha ⟨h₁a, h₂a⟩
|
||||
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
|
||||
rw [Metric.eventually_nhds_iff_ball] at h₃g
|
||||
|
||||
have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
|
||||
have h₄g : ContinuousAt g a :=
|
||||
AnalyticAt.continuousAt h₁g
|
||||
have : {0}ᶜ ∈ nhds (g a) := 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 hy ⟨h₁y, h₂y⟩ h₃
|
||||
|
||||
have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
|
||||
simp
|
||||
calc dist y a
|
||||
_ < min ε₁ ε₂ := by assumption
|
||||
_ ≤ ε₂ := by exact min_le_right ε₁ ε₂
|
||||
|
||||
have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
|
||||
simp
|
||||
calc dist y a
|
||||
_ < min ε₁ ε₂ := by assumption
|
||||
_ ≤ ε₁ := by exact min_le_left ε₁ ε₂
|
||||
|
||||
have F := h₂ε₂ y h'₂y
|
||||
have : f y = 0 := by
|
||||
rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
|
||||
tauto
|
||||
rw [this] at F
|
||||
simp at F
|
||||
|
||||
have : g y ≠ 0 := by
|
||||
exact h₁ε₁.2 y h₃y
|
||||
simp [this] at F
|
||||
rw [sub_eq_zero] at F
|
||||
tauto
|
||||
|
||||
|
||||
theorem AnalyticOn.support_of_zeroDivisor
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOn ℂ f U) :
|
||||
Function.support hf.zeroDivisor ⊆ U := by
|
||||
|
||||
intro z
|
||||
contrapose
|
||||
intro hz
|
||||
dsimp [AnalyticOn.zeroDivisor]
|
||||
simp
|
||||
tauto
|
||||
|
||||
|
||||
theorem AnalyticOn.support_of_zeroDivisor₂
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hf : AnalyticOn ℂ f U) :
|
||||
Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
|
||||
|
||||
intro z hz
|
||||
dsimp [AnalyticOn.zeroDivisor] at hz
|
||||
have t₀ := hf.support_of_zeroDivisor hz
|
||||
simp [hf.support_of_zeroDivisor hz] at hz
|
||||
let A := hz.1
|
||||
let C := (hf z t₀).order_eq_zero_iff
|
||||
simp
|
||||
rw [C] at A
|
||||
tauto
|
|
@ -1,21 +0,0 @@
|
|||
import Mathlib.Analysis.Analytic.Meromorphic
|
||||
import Nevanlinna.holomorphic_JensenFormula
|
||||
|
||||
open Real
|
||||
|
||||
variable (f : ℂ → ℂ)
|
||||
variable {h₁f : MeromorphicOn f ⊤}
|
||||
variable {h₂f : f 0 ≠ 0}
|
||||
|
||||
|
||||
|
||||
noncomputable def Nevanlinna.n : ℝ → ℤ := by
|
||||
intro r
|
||||
have : MeromorphicAt f z := by
|
||||
exact h₁f (sorryAx ℂ true) trivial
|
||||
exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
|
||||
|
||||
noncomputable def integratedCounting : ℝ → ℝ := by
|
||||
intro r
|
||||
-- Issue here: for s on the boundary of the ball, zero comes out.
|
||||
exact ∑ᶠ s, (h₁f.order s).toNat * log (r * ‖s.1‖⁻¹)
|
|
@ -1,5 +1,5 @@
|
|||
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
|
||||
import Nevanlinna.harmonicAt
|
||||
import Nevanlinna.complexHarmonic
|
||||
import Nevanlinna.holomorphicAt
|
||||
|
||||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
|
|
@ -1,131 +0,0 @@
|
|||
import Mathlib.Analysis.NormedSpace.Pointwise
|
||||
import Mathlib.Topology.MetricSpace.Thickening
|
||||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Nevanlinna.holomorphic_examples
|
||||
|
||||
theorem harmonic_meanValue
|
||||
{f : ℂ → ℝ}
|
||||
{z : ℂ}
|
||||
(ρ R : ℝ)
|
||||
(hR : 0 < R)
|
||||
(hρ : R < ρ)
|
||||
(hf : ∀ x ∈ Metric.ball z ρ , HarmonicAt f x) :
|
||||
(∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z
|
||||
:= by
|
||||
|
||||
obtain ⟨F, h₁F, h₂F⟩ := harmonic_is_realOfHolomorphic (gt_trans hρ hR) hf
|
||||
|
||||
have hrρ : Metric.ball z R ⊆ Metric.ball z ρ := by
|
||||
intro x hx
|
||||
exact gt_trans hρ hx
|
||||
|
||||
have reg₀F : DifferentiableOn ℂ F (Metric.ball z ρ) := by
|
||||
intro x hx
|
||||
apply DifferentiableAt.differentiableWithinAt
|
||||
apply HolomorphicAt.differentiableAt (h₁F x _)
|
||||
exact hx
|
||||
|
||||
have reg₁F : DifferentiableOn ℂ F (Metric.ball z R) := by
|
||||
intro x hx
|
||||
apply DifferentiableAt.differentiableWithinAt
|
||||
apply HolomorphicAt.differentiableAt (h₁F x _)
|
||||
exact hrρ hx
|
||||
|
||||
have : (∮ (x : ℂ) in C(z, R), (x - z)⁻¹ • F x) = (2 * ↑Real.pi * Complex.I) • F z := by
|
||||
let s : Set ℂ := ∅
|
||||
let hs : s.Countable := Set.countable_empty
|
||||
let _ : ℂ := 0
|
||||
have hw : (z : ℂ) ∈ Metric.ball z R := Metric.mem_ball_self hR
|
||||
have hc : ContinuousOn F (Metric.closedBall z R) := by
|
||||
apply reg₀F.continuousOn.mono
|
||||
intro x hx
|
||||
simp at hx
|
||||
simp
|
||||
linarith
|
||||
have hd : ∀ x ∈ Metric.ball z R \ s, DifferentiableAt ℂ F x := by
|
||||
intro x hx
|
||||
let A := reg₁F x hx.1
|
||||
apply A.differentiableAt
|
||||
apply (IsOpen.mem_nhds_iff ?hs).mpr
|
||||
exact hx.1
|
||||
exact Metric.isOpen_ball
|
||||
let CIF := Complex.circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
|
||||
simp at CIF
|
||||
assumption
|
||||
|
||||
unfold circleIntegral at this
|
||||
simp_rw [deriv_circleMap] at this
|
||||
|
||||
have t₁ {θ : ℝ} : (circleMap 0 R θ * Complex.I) • (circleMap 0 R θ)⁻¹ • F (circleMap z R θ) = Complex.I • F (circleMap z R θ) := by
|
||||
rw [← smul_assoc]
|
||||
congr 1
|
||||
simp
|
||||
nth_rw 1 [mul_comm]
|
||||
rw [← mul_assoc]
|
||||
simp
|
||||
apply inv_mul_cancel₀
|
||||
apply circleMap_ne_center
|
||||
exact Ne.symm (ne_of_lt hR)
|
||||
have t'₁ {θ : ℝ} : circleMap 0 R θ = circleMap z R θ - z := by
|
||||
exact Eq.symm (circleMap_sub_center z R θ)
|
||||
simp_rw [← t'₁, t₁] at this
|
||||
simp at this
|
||||
|
||||
have t₂ : Complex.reCLM (-Complex.I * (Complex.I * ∫ (x : ℝ) in (0)..2 * Real.pi, F (circleMap z R x))) = Complex.reCLM (-Complex.I * (2 * ↑Real.pi * Complex.I * F z)) := by
|
||||
rw [this]
|
||||
simp at t₂
|
||||
have xx {x : ℝ} : (F (circleMap z R x)).re = f (circleMap z R x) := by
|
||||
rw [← h₂F]
|
||||
simp
|
||||
simp
|
||||
rw [Complex.dist_eq]
|
||||
rw [circleMap_sub_center]
|
||||
simp
|
||||
rwa [abs_of_nonneg (le_of_lt hR)]
|
||||
have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
|
||||
rw [x₁] at t₂
|
||||
rw [← ContinuousLinearMap.intervalIntegral_comp_comm] at t₂
|
||||
simp at t₂
|
||||
simp_rw [xx] at t₂
|
||||
have x₁ {z : ℂ} : z.re = Complex.reCLM z := by rfl
|
||||
rw [x₁] at t₂
|
||||
have : Complex.reCLM (F z) = f z := by
|
||||
apply h₂F
|
||||
simp
|
||||
exact gt_trans hρ hR
|
||||
rw [this] at t₂
|
||||
exact t₂
|
||||
|
||||
-- IntervalIntegrable (fun x => F (circleMap 0 1 x)) MeasureTheory.volume 0 (2 * Real.pi)
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp reg₀F.continuousOn _
|
||||
intro θ _
|
||||
simp
|
||||
rw [Complex.dist_eq, circleMap_sub_center]
|
||||
simp
|
||||
rwa [abs_of_nonneg (le_of_lt hR)]
|
||||
apply Continuous.continuousOn
|
||||
exact continuous_circleMap z R
|
||||
|
||||
/- Probably not optimal yet. We want a statements that requires harmonicity in
|
||||
the interior and continuity on the closed ball.
|
||||
-/
|
||||
|
||||
|
||||
theorem harmonic_meanValue₁
|
||||
{f : ℂ → ℝ}
|
||||
{z : ℂ}
|
||||
(R : ℝ)
|
||||
(hR : 0 < R)
|
||||
(hf : ∀ x ∈ Metric.closedBall z R , HarmonicAt f x) :
|
||||
(∫ (x : ℝ) in (0)..2 * Real.pi, f (circleMap z R x)) = 2 * Real.pi * f z := by
|
||||
|
||||
obtain ⟨e, h₁e, h₂e⟩ := IsCompact.exists_thickening_subset_open (isCompact_closedBall z R) (HarmonicAt_isOpen f) hf
|
||||
rw [thickening_closedBall] at h₂e
|
||||
apply harmonic_meanValue (e + R) R
|
||||
assumption
|
||||
norm_num
|
||||
assumption
|
||||
exact fun x a => h₂e a
|
||||
assumption
|
||||
linarith
|
|
@ -2,8 +2,8 @@ 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]
|
||||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
|
||||
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G]
|
||||
|
||||
def HolomorphicAt (f : E → F) (x : E) : Prop :=
|
||||
∃ s ∈ nhds x, ∀ z ∈ s, DifferentiableAt ℂ f z
|
||||
|
@ -33,21 +33,6 @@ theorem HolomorphicAt_iff
|
|||
· 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} :
|
||||
|
@ -120,7 +105,6 @@ theorem HolomorphicAt_neg
|
|||
|
||||
|
||||
theorem HolomorphicAt_contDiffAt
|
||||
[CompleteSpace F]
|
||||
{f : ℂ → F}
|
||||
{z : ℂ}
|
||||
(hf : HolomorphicAt f z) :
|
||||
|
@ -153,11 +137,12 @@ theorem CauchyRiemann'₅
|
|||
simp
|
||||
rw [← mul_one Complex.I]
|
||||
rw [← smul_eq_mul]
|
||||
rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1]
|
||||
conv =>
|
||||
right
|
||||
right
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||||
simp
|
||||
|
||||
|
||||
theorem CauchyRiemann'₆
|
||||
{f : ℂ → F}
|
||||
|
|
|
@ -3,10 +3,8 @@ 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) :=
|
||||
|
@ -27,7 +25,6 @@ theorem partialDeriv_compContLinAt
|
|||
rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
|
||||
simp
|
||||
|
||||
|
||||
theorem partialDeriv_compCLE
|
||||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
|
||||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||||
|
@ -88,7 +85,7 @@ theorem partialDeriv_smul'₂
|
|||
theorem CauchyRiemann₄
|
||||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||||
{f : ℂ → F} :
|
||||
(Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by
|
||||
(Differentiable ℂ f) → partialDeriv Complex.I f = Complex.I • partialDeriv 1 f := by
|
||||
intro h
|
||||
unfold partialDeriv
|
||||
|
||||
|
@ -99,14 +96,12 @@ theorem CauchyRiemann₄
|
|||
simp
|
||||
rw [← mul_one Complex.I]
|
||||
rw [← smul_eq_mul]
|
||||
rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1]
|
||||
conv =>
|
||||
right
|
||||
right
|
||||
intro w
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)]
|
||||
funext w
|
||||
simp
|
||||
-/
|
||||
|
||||
|
||||
theorem MeasureTheory.integral2_divergence₃
|
||||
|
@ -208,9 +203,9 @@ theorem integral_divergence₅
|
|||
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
|
||||
have {z : ℂ} : fderiv ℝ F z Complex.I = partialDeriv _ 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
|
||||
have {z : ℂ} : fderiv ℝ (-Complex.I • F) z 1 = partialDeriv _ (-Complex.I • F) z := by rfl
|
||||
conv at A in (fderiv ℝ (-Complex.I • F) _) _ => rw [this]
|
||||
conv at A =>
|
||||
left
|
||||
|
@ -296,17 +291,26 @@ theorem primitive_fderivAtBasepointZero
|
|||
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
|
||||
apply Continuous.comp
|
||||
exact hf
|
||||
have : ((fun x => { re := a, im := x }) : ℝ → ℂ) = (fun x => { re := a, im := 0 } + { re := 0, im := x }) := by
|
||||
funext x
|
||||
apply Complex.ext
|
||||
rw [Complex.add_re]
|
||||
simp
|
||||
rw [Complex.add_im]
|
||||
simp
|
||||
rw [this]
|
||||
apply Continuous.add
|
||||
continuity
|
||||
fun_prop
|
||||
have : (fun x => { re := 0, im := x } : ℝ → ℂ) = Complex.I • Complex.ofRealCLM := by
|
||||
funext x
|
||||
simp
|
||||
have : (x : ℂ) = {re := x, im := 0} := by rfl
|
||||
rw [this]
|
||||
rw [Complex.I_mul]
|
||||
simp
|
||||
continuity
|
||||
|
||||
have t₃ {a : ℝ} : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 a := by
|
||||
apply Continuous.intervalIntegrable
|
||||
|
@ -485,11 +489,11 @@ theorem primitive_translation
|
|||
simp
|
||||
|
||||
|
||||
theorem primitive_hasDerivAtBasepoint
|
||||
theorem primitive_fderivAtBasepoint
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
(hf : Continuous f)
|
||||
(z₀ : ℂ) :
|
||||
{z₀ : ℂ}
|
||||
(f : ℂ → E)
|
||||
(hf : Continuous f) :
|
||||
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
|
||||
|
||||
let g := f ∘ fun z ↦ z + z₀
|
||||
|
@ -553,7 +557,7 @@ lemma integrability₂
|
|||
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
|
||||
have : ((fun x => { re := b, im := x }) : ℝ → ℂ) = (fun x => Complex.I • Complex.ofRealCLM x + { re := b, im := 0 }) := by
|
||||
funext x
|
||||
apply Complex.ext
|
||||
rw [Complex.add_re]
|
||||
|
@ -597,70 +601,15 @@ theorem primitive_additivity
|
|||
abel
|
||||
|
||||
|
||||
theorem primitive_hasDerivAt
|
||||
theorem primitive_fderiv
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
(hf : Differentiable ℂ f)
|
||||
(z₀ z : ℂ) :
|
||||
{z₀ z : ℂ}
|
||||
(f : ℂ → E)
|
||||
(hf : Differentiable ℂ f) :
|
||||
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
|
||||
apply primitive_fderivAtBasepoint
|
||||
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
|
||||
|
|
@ -1,4 +1,4 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Complex.TaylorSeries
|
||||
import Nevanlinna.cauchyRiemann
|
||||
|
||||
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
|
||||
|
@ -33,21 +33,6 @@ theorem HolomorphicAt_iff
|
|||
· assumption
|
||||
|
||||
|
||||
theorem Differentiable.holomorphicAt
|
||||
{f : E → F}
|
||||
(hf : Differentiable ℂ f)
|
||||
{x : E} :
|
||||
HolomorphicAt f x := by
|
||||
apply HolomorphicAt_iff.2
|
||||
use Set.univ
|
||||
constructor
|
||||
· exact isOpen_univ
|
||||
· constructor
|
||||
· exact trivial
|
||||
· intro z _
|
||||
exact hf z
|
||||
|
||||
|
||||
theorem HolomorphicAt_isOpen
|
||||
(f : E → F) :
|
||||
IsOpen { x : E | HolomorphicAt f x } := by
|
||||
|
@ -110,38 +95,6 @@ theorem HolomorphicAt_neg
|
|||
exact h₂UF z hz
|
||||
|
||||
|
||||
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 AnalyticAt.holomorphicAt
|
||||
[CompleteSpace F]
|
||||
{f : ℂ → F}
|
||||
{x : ℂ} :
|
||||
AnalyticAt ℂ f x → HolomorphicAt f x := by
|
||||
intro hf
|
||||
rw [HolomorphicAt_iff]
|
||||
use {x : ℂ | AnalyticAt ℂ f x}
|
||||
constructor
|
||||
· exact isOpen_analyticAt ℂ f
|
||||
· constructor
|
||||
· simpa
|
||||
· intro z hz
|
||||
simp at hz
|
||||
exact differentiableAt hz
|
||||
|
||||
|
||||
theorem HolomorphicAt.contDiffAt
|
||||
[CompleteSpace F]
|
||||
{f : ℂ → F}
|
||||
|
|
|
@ -1,449 +0,0 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
import Mathlib.Analysis.Analytic.IsolatedZeros
|
||||
import Nevanlinna.analyticOn_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 : 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
|
||||
|
||||
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⟩ := AnalyticOnCompact.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 [AnalyticOn.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 (AnalyticOn.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 : 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 ℓ : ℂ ≃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 : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
|
||||
apply AnalyticOn.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 [AnalyticOn.order]
|
||||
rw [← AnalyticAt.order_comp_CLE ℓ]
|
||||
|
||||
--
|
||||
simpa
|
||||
--
|
||||
have : R = |R| := by exact Eq.symm (abs_of_pos hR)
|
||||
rw [← this]
|
||||
apply inv_ne_zero
|
||||
exact Ne.symm (ne_of_lt hR)
|
||||
--
|
||||
exact Ne.symm (ne_of_lt hR)
|
||||
--
|
||||
simp
|
||||
constructor
|
||||
· assumption
|
||||
· exact Ne.symm (ne_of_lt hR)
|
|
@ -1,314 +0,0 @@
|
|||
import Nevanlinna.harmonicAt
|
||||
import Nevanlinna.holomorphicAt
|
||||
import Nevanlinna.holomorphic_primitive
|
||||
import Nevanlinna.mathlibAddOn
|
||||
|
||||
|
||||
theorem CauchyRiemann₆
|
||||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E]
|
||||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||||
{f : E → F}
|
||||
{z : E} :
|
||||
(DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ ∀ e, partialDeriv ℝ (Complex.I • e) f z = Complex.I • partialDeriv ℝ e f z := by
|
||||
constructor
|
||||
|
||||
· -- Direction "→"
|
||||
intro h
|
||||
constructor
|
||||
· exact DifferentiableAt.restrictScalars ℝ h
|
||||
· unfold partialDeriv
|
||||
conv =>
|
||||
intro e
|
||||
left
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||||
simp
|
||||
rw [← mul_one Complex.I]
|
||||
rw [← smul_eq_mul]
|
||||
conv =>
|
||||
intro e
|
||||
right
|
||||
right
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ h]
|
||||
simp
|
||||
|
||||
· -- Direction "←"
|
||||
intro ⟨h₁, h₂⟩
|
||||
apply (differentiableAt_iff_restrictScalars ℝ h₁).2
|
||||
|
||||
use {
|
||||
toFun := fderiv ℝ f z
|
||||
map_add' := fun x y => ContinuousLinearMap.map_add (fderiv ℝ f z) x y
|
||||
map_smul' := by
|
||||
simp
|
||||
intro m x
|
||||
have : m = m.re + m.im • Complex.I := by simp
|
||||
rw [this, add_smul, add_smul, ContinuousLinearMap.map_add]
|
||||
congr
|
||||
simp
|
||||
rw [smul_assoc, smul_assoc, ContinuousLinearMap.map_smul (fderiv ℝ f z) m.2]
|
||||
congr
|
||||
exact h₂ x
|
||||
}
|
||||
rfl
|
||||
|
||||
|
||||
theorem CauchyRiemann₇
|
||||
{F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F]
|
||||
{f : ℂ → F}
|
||||
{z : ℂ} :
|
||||
(DifferentiableAt ℂ f z) ↔ (DifferentiableAt ℝ f z) ∧ partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by
|
||||
constructor
|
||||
· intro hf
|
||||
constructor
|
||||
· exact (CauchyRiemann₆.1 hf).1
|
||||
· let A := (CauchyRiemann₆.1 hf).2 1
|
||||
simp at A
|
||||
exact A
|
||||
· intro ⟨h₁, h₂⟩
|
||||
apply CauchyRiemann₆.2
|
||||
constructor
|
||||
· exact h₁
|
||||
· intro e
|
||||
have : Complex.I • e = e • Complex.I := by
|
||||
rw [smul_eq_mul, smul_eq_mul]
|
||||
exact CommMonoid.mul_comm Complex.I e
|
||||
rw [this]
|
||||
have : e = e.re + e.im • Complex.I := by simp
|
||||
rw [this, add_smul, partialDeriv_add₁, partialDeriv_add₁]
|
||||
simp
|
||||
rw [← smul_eq_mul]
|
||||
have : partialDeriv ℝ ((e.re : ℝ) • Complex.I) f = partialDeriv ℝ ((e.re : ℂ) • Complex.I) f := by rfl
|
||||
rw [← this, partialDeriv_smul₁ ℝ]
|
||||
have : (e.re : ℂ) = (e.re : ℝ) • (1 : ℂ) := by simp
|
||||
rw [this, partialDeriv_smul₁ ℝ]
|
||||
have : partialDeriv ℝ ((e.im : ℂ) * Complex.I) f = partialDeriv ℝ ((e.im : ℝ) • Complex.I) f := by rfl
|
||||
rw [this, partialDeriv_smul₁ ℝ]
|
||||
simp
|
||||
rw [h₂]
|
||||
rw [smul_comm]
|
||||
congr
|
||||
rw [mul_assoc]
|
||||
simp
|
||||
nth_rw 2 [smul_comm]
|
||||
rw [← smul_assoc]
|
||||
simp
|
||||
have : - (e.im : ℂ) = (-e.im : ℝ) • (1 : ℂ) := by simp
|
||||
rw [this, partialDeriv_smul₁ ℝ]
|
||||
simp
|
||||
|
||||
|
||||
|
||||
|
||||
/-
|
||||
|
||||
A harmonic, real-valued function on ℂ is the real part of a suitable holomorphic
|
||||
function.
|
||||
|
||||
-/
|
||||
|
||||
theorem harmonic_is_realOfHolomorphic
|
||||
{f : ℂ → ℝ}
|
||||
{z : ℂ}
|
||||
{R : ℝ}
|
||||
(hR : 0 < R)
|
||||
(hf : ∀ x ∈ Metric.ball z R, HarmonicAt f x) :
|
||||
∃ F : ℂ → ℂ, (∀ x ∈ Metric.ball z R, HolomorphicAt F x) ∧ (Set.EqOn (Complex.reCLM ∘ F) f (Metric.ball z R)) := by
|
||||
|
||||
let f_1 : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ 1 f)
|
||||
let f_I : ℂ → ℂ := Complex.ofRealCLM ∘ (partialDeriv ℝ Complex.I f)
|
||||
|
||||
let g : ℂ → ℂ := f_1 - Complex.I • f_I
|
||||
|
||||
have contDiffOn_if_contDiffAt
|
||||
{f' : ℂ → ℝ}
|
||||
{z' : ℂ}
|
||||
{R' : ℝ}
|
||||
{n' : ℕ}
|
||||
(hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
|
||||
ContDiffOn ℝ n' f' (Metric.ball z' R') := by
|
||||
intro z hz
|
||||
apply ContDiffAt.contDiffWithinAt
|
||||
exact hf' z hz
|
||||
|
||||
have reg₂f : ContDiffOn ℝ 2 f (Metric.ball z R) := by
|
||||
apply contDiffOn_if_contDiffAt
|
||||
intro x hx
|
||||
exact (hf x hx).1
|
||||
|
||||
have contDiffOn_if_contDiffAt'
|
||||
{f' : ℂ → ℂ}
|
||||
{z' : ℂ}
|
||||
{R' : ℝ}
|
||||
{n' : ℕ}
|
||||
(hf' : ∀ x ∈ Metric.ball z' R', ContDiffAt ℝ n' f' x) :
|
||||
ContDiffOn ℝ n' f' (Metric.ball z' R') := by
|
||||
intro z hz
|
||||
apply ContDiffAt.contDiffWithinAt
|
||||
exact hf' z hz
|
||||
|
||||
have reg₁f_1 : ContDiffOn ℝ 1 f_1 (Metric.ball z R) := by
|
||||
apply contDiffOn_if_contDiffAt'
|
||||
intro z hz
|
||||
dsimp [f_1]
|
||||
apply ContDiffAt.continuousLinearMap_comp
|
||||
exact partialDeriv_contDiffAt ℝ (hf z hz).1 1
|
||||
|
||||
have reg₁f_I : ContDiffOn ℝ 1 f_I (Metric.ball z R) := by
|
||||
apply contDiffOn_if_contDiffAt'
|
||||
intro z hz
|
||||
dsimp [f_I]
|
||||
apply ContDiffAt.continuousLinearMap_comp
|
||||
exact partialDeriv_contDiffAt ℝ (hf z hz).1 Complex.I
|
||||
|
||||
have reg₁g : ContDiffOn ℝ 1 g (Metric.ball z R) := by
|
||||
dsimp [g]
|
||||
apply ContDiffOn.sub
|
||||
exact reg₁f_1
|
||||
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
|
||||
rw [this]
|
||||
apply ContDiffOn.const_smul
|
||||
exact reg₁f_I
|
||||
|
||||
have reg₁ : DifferentiableOn ℂ g (Metric.ball z R) := by
|
||||
intro x hx
|
||||
apply DifferentiableAt.differentiableWithinAt
|
||||
apply CauchyRiemann₇.2
|
||||
constructor
|
||||
· apply DifferentiableWithinAt.differentiableAt (reg₁g.differentiableOn le_rfl x hx)
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
· dsimp [g]
|
||||
rw [partialDeriv_sub₂_differentiableAt, partialDeriv_sub₂_differentiableAt]
|
||||
dsimp [f_1, f_I]
|
||||
rw [partialDeriv_smul'₂, partialDeriv_smul'₂]
|
||||
rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
|
||||
simp
|
||||
rw [partialDeriv_compContLinAt, partialDeriv_compContLinAt]
|
||||
rw [mul_sub]
|
||||
simp
|
||||
rw [← mul_assoc]
|
||||
simp
|
||||
rw [add_comm, sub_eq_add_neg]
|
||||
congr 1
|
||||
· rw [partialDeriv_commOn _ reg₂f Complex.I 1]
|
||||
exact hx
|
||||
exact Metric.isOpen_ball
|
||||
· let A := Filter.EventuallyEq.eq_of_nhds (hf x hx).2
|
||||
simp at A
|
||||
unfold Complex.laplace at A
|
||||
conv =>
|
||||
right
|
||||
right
|
||||
rw [← sub_zero (partialDeriv ℝ 1 (partialDeriv ℝ 1 f) x)]
|
||||
rw [← A]
|
||||
simp
|
||||
|
||||
--DifferentiableAt ℝ (partialDeriv ℝ _ f)
|
||||
repeat
|
||||
apply ContDiffAt.differentiableAt
|
||||
apply partialDeriv_contDiffAt ℝ (hf x hx).1
|
||||
apply le_rfl
|
||||
|
||||
-- DifferentiableAt ℝ f_1 x
|
||||
apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
|
||||
-- DifferentiableAt ℝ (Complex.I • f_I)
|
||||
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
|
||||
rw [this]
|
||||
apply DifferentiableAt.const_smul
|
||||
apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
|
||||
-- Differentiable ℝ f_1
|
||||
apply (reg₁f_1.differentiableOn le_rfl).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
|
||||
-- Differentiable ℝ (Complex.I • f_I)
|
||||
have : Complex.I • f_I = fun x ↦ Complex.I • f_I x := by rfl
|
||||
rw [this]
|
||||
apply DifferentiableAt.const_smul
|
||||
apply (reg₁f_I.differentiableOn le_rfl).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
|
||||
let F := fun z' ↦ (primitive z g) z' + f z
|
||||
|
||||
have regF : DifferentiableOn ℂ F (Metric.ball z R) := by
|
||||
apply DifferentiableOn.add
|
||||
apply primitive_differentiableOn reg₁
|
||||
simp
|
||||
|
||||
have pF'' : ∀ x ∈ Metric.ball z R, (fderiv ℝ F x) = ContinuousLinearMap.lsmul ℝ ℂ (g x) := by
|
||||
intro x hx
|
||||
have : DifferentiableAt ℂ F x := by
|
||||
apply (regF x hx).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
rw [DifferentiableAt.fderiv_restrictScalars ℝ this]
|
||||
dsimp [F]
|
||||
rw [fderiv_add_const]
|
||||
rw [primitive_fderiv' reg₁ x hx]
|
||||
exact rfl
|
||||
|
||||
use F
|
||||
|
||||
constructor
|
||||
· -- ∀ x ∈ Metric.ball z R, HolomorphicAt F x
|
||||
intro x hx
|
||||
apply HolomorphicAt_iff.2
|
||||
use Metric.ball z R
|
||||
constructor
|
||||
· exact Metric.isOpen_ball
|
||||
· constructor
|
||||
· assumption
|
||||
· intro w hw
|
||||
apply (regF w hw).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hw
|
||||
· -- Set.EqOn (⇑Complex.reCLM ∘ F) f (Metric.ball z R)
|
||||
have : DifferentiableOn ℝ (Complex.reCLM ∘ F) (Metric.ball z R) := by
|
||||
apply DifferentiableOn.comp
|
||||
apply Differentiable.differentiableOn
|
||||
apply ContinuousLinearMap.differentiable Complex.reCLM
|
||||
apply regF.restrictScalars ℝ
|
||||
exact Set.mapsTo'.mpr fun ⦃a⦄ _ => hR
|
||||
have hz : z ∈ Metric.ball z R := by exact Metric.mem_ball_self hR
|
||||
apply Convex.eqOn_of_fderivWithin_eq _ this _ _ _ hz _
|
||||
exact convex_ball z R
|
||||
apply reg₂f.differentiableOn one_le_two
|
||||
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
|
||||
|
||||
intro x hx
|
||||
rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
|
||||
rw [fderiv.comp]
|
||||
simp
|
||||
apply ContinuousLinearMap.ext
|
||||
intro w
|
||||
simp
|
||||
rw [pF'']
|
||||
dsimp [g, f_1, f_I, partialDeriv]
|
||||
simp
|
||||
have : w = w.re • 1 + w.im • Complex.I := by simp
|
||||
nth_rw 3 [this]
|
||||
rw [(fderiv ℝ f x).map_add]
|
||||
rw [(fderiv ℝ f x).map_smul, (fderiv ℝ f x).map_smul]
|
||||
rw [smul_eq_mul, smul_eq_mul]
|
||||
ring
|
||||
|
||||
assumption
|
||||
exact ContinuousLinearMap.differentiableAt Complex.reCLM
|
||||
apply (regF.restrictScalars ℝ x hx).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
|
||||
assumption
|
||||
apply (reg₂f.differentiableOn one_le_two).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
apply IsOpen.uniqueDiffOn Metric.isOpen_ball
|
||||
assumption
|
||||
-- DifferentiableAt ℝ (⇑Complex.reCLM ∘ F) x
|
||||
apply DifferentiableAt.comp
|
||||
apply Differentiable.differentiableAt
|
||||
exact ContinuousLinearMap.differentiable Complex.reCLM
|
||||
apply (regF.restrictScalars ℝ x hx).differentiableAt
|
||||
apply IsOpen.mem_nhds Metric.isOpen_ball hx
|
||||
--
|
||||
dsimp [F]
|
||||
rw [primitive_zeroAtBasepoint]
|
||||
simp
|
|
@ -1,846 +0,0 @@
|
|||
import Mathlib.Analysis.Complex.TaylorSeries
|
||||
import Mathlib.Data.ENNReal.Basic
|
||||
|
||||
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}
|
||||
{R : ℝ}
|
||||
(hR : 0 < R)
|
||||
(hf : ContinuousOn f (Metric.ball 0 R)) :
|
||||
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]
|
||||
|
||||
obtain ⟨s, h₁s, h₂s⟩ : ∃ s ⊆ f⁻¹' Metric.ball (f 0) (c / (4 : ℝ)), IsOpen s ∧ 0 ∈ s := by
|
||||
apply eventually_nhds_iff.mp
|
||||
apply continuousAt_def.1
|
||||
apply Continuous.continuousAt
|
||||
fun_prop
|
||||
|
||||
apply continuousAt_def.1
|
||||
apply hf.continuousAt
|
||||
exact Metric.ball_mem_nhds 0 hR
|
||||
apply Metric.ball_mem_nhds (f 0)
|
||||
simpa
|
||||
|
||||
obtain ⟨ε, h₁ε, h₂ε⟩ : ∃ ε > 0, (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ s ∧ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε) ⊆ Metric.ball 0 R := by
|
||||
obtain ⟨ε', h₁ε', h₂ε'⟩ : ∃ ε' > 0, Metric.ball 0 ε' ⊆ s ∩ Metric.ball 0 R := by
|
||||
apply Metric.mem_nhds_iff.mp
|
||||
apply IsOpen.mem_nhds
|
||||
apply IsOpen.inter
|
||||
exact h₂s.1
|
||||
exact Metric.isOpen_ball
|
||||
constructor
|
||||
· exact h₂s.2
|
||||
· simpa
|
||||
|
||||
use (2 : ℝ)⁻¹ * ε'
|
||||
|
||||
constructor
|
||||
· simpa
|
||||
· constructor
|
||||
· intro x hx
|
||||
apply (h₂ε' _).1
|
||||
simp
|
||||
calc Complex.abs x
|
||||
_ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
|
||||
_ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
|
||||
apply (add_lt_add_iff_right |x.im|).mpr
|
||||
have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
|
||||
simp at this
|
||||
exact this
|
||||
_ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
|
||||
apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
|
||||
have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
|
||||
simp at this
|
||||
exact this
|
||||
_ = ε' := by
|
||||
rw [← add_mul]
|
||||
abel_nf
|
||||
simp
|
||||
· intro x hx
|
||||
apply (h₂ε' _).2
|
||||
simp
|
||||
calc Complex.abs x
|
||||
_ ≤ |x.re| + |x.im| := Complex.abs_le_abs_re_add_abs_im x
|
||||
_ < (2 : ℝ)⁻¹ * ε' + |x.im| := by
|
||||
apply (add_lt_add_iff_right |x.im|).mpr
|
||||
have : x.re ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).1
|
||||
simp at this
|
||||
exact this
|
||||
_ < (2 : ℝ)⁻¹ * ε' + (2 : ℝ)⁻¹ * ε' := by
|
||||
apply (add_lt_add_iff_left ((2 : ℝ)⁻¹ * ε')).mpr
|
||||
have : x.im ∈ Metric.ball 0 (2⁻¹ * ε') := (Complex.mem_reProdIm.1 hx).2
|
||||
simp at this
|
||||
exact this
|
||||
_ = ε' := by
|
||||
rw [← add_mul]
|
||||
abel_nf
|
||||
simp
|
||||
|
||||
have h₃ε : ∀ y ∈ (Metric.ball 0 ε) ×ℂ (Metric.ball 0 ε), ‖(f y) - (f 0)‖ < (c / (4 : ℝ)) := by
|
||||
intro y hy
|
||||
apply mem_ball_iff_norm.mp
|
||||
apply h₁s
|
||||
exact h₂ε.1 hy
|
||||
|
||||
|
||||
have intervalComputation_uIcc {x' y' : ℝ} (h : x' ∈ Set.uIcc 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
|
||||
rwa [abs_of_nonneg A, abs_of_nonneg hy]
|
||||
· simp [hy] at A
|
||||
simp [hy] at B
|
||||
rw [abs_of_nonpos hy]
|
||||
rw [abs_of_nonpos]
|
||||
linarith [h.1]
|
||||
exact B
|
||||
|
||||
|
||||
rw [Filter.eventually_iff_exists_mem]
|
||||
use Metric.ball 0 (ε / (4 : ℝ))
|
||||
|
||||
constructor
|
||||
· apply Metric.ball_mem_nhds 0
|
||||
linarith
|
||||
· intro y hy
|
||||
|
||||
have {A B C D :E} : (A + B) - (C + D) = (A - C) + (B - D) := by
|
||||
abel
|
||||
rw [this]
|
||||
rw [← smul_sub]
|
||||
|
||||
|
||||
have t₀ : IntervalIntegrable (fun x => f { re := x, im := 0 }) MeasureTheory.volume 0 y.re := by
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf
|
||||
have : (fun x => ({ re := x, im := 0 } : ℂ)) = Complex.ofRealLI := by rfl
|
||||
rw [this]
|
||||
apply Continuous.continuousOn
|
||||
continuity
|
||||
intro x hx
|
||||
apply h₂ε.2
|
||||
simp
|
||||
constructor
|
||||
· simp
|
||||
calc |x|
|
||||
_ ≤ |y.re| := by apply intervalComputation_uIcc hx
|
||||
_ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
|
||||
_ < ε / 4 := by simp at hy; assumption
|
||||
_ < ε := by linarith
|
||||
· simpa
|
||||
have t₁ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.re := by
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
apply hf
|
||||
fun_prop
|
||||
intro x _
|
||||
simpa
|
||||
rw [← intervalIntegral.integral_sub t₀ t₁]
|
||||
|
||||
have t₂ : IntervalIntegrable (fun x_1 => f { re := y.re, im := x_1 }) MeasureTheory.volume 0 y.im := by
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf
|
||||
have : (Complex.mk y.re) = (fun x => Complex.I • Complex.ofRealCLM x + { re := y.re, im := 0 }) := by
|
||||
funext x
|
||||
apply Complex.ext
|
||||
rw [Complex.add_re]
|
||||
simp
|
||||
simp
|
||||
rw [this]
|
||||
apply ContinuousOn.add
|
||||
apply Continuous.continuousOn
|
||||
continuity
|
||||
fun_prop
|
||||
intro x hx
|
||||
apply h₂ε.2
|
||||
constructor
|
||||
· simp
|
||||
calc |y.re|
|
||||
_ ≤ Complex.abs y := by exact Complex.abs_re_le_abs y
|
||||
_ < ε / 4 := by simp at hy; assumption
|
||||
_ < ε := by linarith
|
||||
· simp
|
||||
calc |x|
|
||||
_ ≤ |y.im| := by apply intervalComputation_uIcc hx
|
||||
_ ≤ Complex.abs y := by exact Complex.abs_im_le_abs y
|
||||
_ < ε / 4 := by simp at hy; assumption
|
||||
_ < ε := by linarith
|
||||
have t₃ : IntervalIntegrable (fun _ => f 0) MeasureTheory.volume 0 y.im := by
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf
|
||||
fun_prop
|
||||
intro x _
|
||||
apply h₂ε.2
|
||||
simp
|
||||
constructor
|
||||
· simpa
|
||||
· simpa
|
||||
rw [← intervalIntegral.integral_sub t₂ t₃]
|
||||
|
||||
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 }
|
||||
constructor
|
||||
· simp
|
||||
linarith
|
||||
· simp
|
||||
exact h₁ε
|
||||
|
||||
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 }
|
||||
constructor
|
||||
· simp
|
||||
linarith
|
||||
· simp
|
||||
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}
|
||||
{R : ℝ}
|
||||
(z₀ : ℂ)
|
||||
(hR : 0 < R)
|
||||
(hf : ContinuousOn f (Metric.ball z₀ R)) :
|
||||
HasDerivAt (primitive z₀ f) (f z₀) z₀ := by
|
||||
|
||||
let g := f ∘ fun z ↦ z + z₀
|
||||
have hg : ContinuousOn g (Metric.ball 0 R) := by
|
||||
apply ContinuousOn.comp
|
||||
fun_prop
|
||||
fun_prop
|
||||
intro x hx
|
||||
simp
|
||||
simp at hx
|
||||
assumption
|
||||
|
||||
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₀) := (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 primitive_fderivAtBasepointZero hR hg
|
||||
apply HasDerivAt.sub_const
|
||||
have : (fun (x : ℂ) ↦ x) = id := by
|
||||
funext x
|
||||
simp
|
||||
rw [this]
|
||||
exact hasDerivAt_id z₀
|
||||
|
||||
|
||||
theorem primitive_additivity
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
{z₀ : ℂ}
|
||||
{rx ry : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
|
||||
(hry : 0 < ry)
|
||||
{z₁ : ℂ}
|
||||
(hz₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry))
|
||||
:
|
||||
∃ εx > 0, ∃ εy > 0, ∀ z ∈ (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy), (primitive z₀ f z) - (primitive z₁ f z) - (primitive z₀ f z₁) = 0 := by
|
||||
|
||||
let εx := rx - dist z₀.re z₁.re
|
||||
have hεx : εx > 0 := by
|
||||
let A := hz₁.1
|
||||
simp at A
|
||||
dsimp [εx]
|
||||
rw [dist_comm]
|
||||
simpa
|
||||
let εy := ry - dist z₀.im z₁.im
|
||||
have hεy : εy > 0 := by
|
||||
let A := hz₁.2
|
||||
simp at A
|
||||
dsimp [εy]
|
||||
rw [dist_comm]
|
||||
simpa
|
||||
|
||||
use εx
|
||||
use hεx
|
||||
use εy
|
||||
use hεy
|
||||
|
||||
intro z hz
|
||||
|
||||
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]
|
||||
|
||||
-- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₀.re z₁.re
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf.continuousOn
|
||||
have {b : ℝ} : ((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
|
||||
apply Continuous.continuousOn
|
||||
rw [this]
|
||||
continuity
|
||||
-- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₀.re z₁.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
|
||||
intro w hw
|
||||
simp
|
||||
apply Complex.mem_reProdIm.mpr
|
||||
constructor
|
||||
· simp
|
||||
calc dist w z₀.re
|
||||
_ ≤ dist z₁.re z₀.re := by apply Real.dist_right_le_of_mem_uIcc; rwa [Set.uIcc_comm] at hw
|
||||
_ < rx := by apply Metric.mem_ball.mp (Complex.mem_reProdIm.1 hz₁).1
|
||||
· simpa
|
||||
|
||||
-- IntervalIntegrable (fun x => f { re := x, im := z₀.im }) MeasureTheory.volume z₁.re z.re
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf.continuousOn
|
||||
have {b : ℝ} : ((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
|
||||
apply Continuous.continuousOn
|
||||
rw [this]
|
||||
continuity
|
||||
-- Remains: Set.MapsTo (fun x => { re := x, im := z₀.im }) (Set.uIcc z₁.re z.re) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
|
||||
intro w hw
|
||||
simp
|
||||
constructor
|
||||
· simp
|
||||
calc dist w z₀.re
|
||||
_ ≤ dist w z₁.re + dist z₁.re z₀.re := by exact dist_triangle w z₁.re z₀.re
|
||||
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
|
||||
apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
rw [Set.uIcc_comm] at hw
|
||||
exact Real.dist_right_le_of_mem_uIcc hw
|
||||
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
|
||||
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
|
||||
_ = rx := by
|
||||
rw [dist_comm]
|
||||
simp
|
||||
· simpa
|
||||
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]
|
||||
|
||||
-- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₀.im z₁.im
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf.continuousOn
|
||||
apply Continuous.continuousOn
|
||||
have {b : ℝ}: (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
|
||||
fun_prop
|
||||
fun_prop
|
||||
-- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₀.im z₁.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
|
||||
intro w hw
|
||||
constructor
|
||||
· simp
|
||||
calc dist z.re z₀.re
|
||||
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
|
||||
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
|
||||
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
|
||||
_ = rx := by
|
||||
rw [dist_comm]
|
||||
simp
|
||||
· simp
|
||||
calc dist w z₀.im
|
||||
_ ≤ dist z₁.im z₀.im := by rw [Set.uIcc_comm] at hw; exact Real.dist_right_le_of_mem_uIcc hw
|
||||
_ < ry := by
|
||||
rw [← Metric.mem_ball]
|
||||
exact hz₁.2
|
||||
|
||||
-- IntervalIntegrable (fun x => f { re := z.re, im := x }) MeasureTheory.volume z₁.im z.im
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp
|
||||
exact hf.continuousOn
|
||||
apply Continuous.continuousOn
|
||||
have {b : ℝ}: (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
|
||||
fun_prop
|
||||
fun_prop
|
||||
-- Set.MapsTo (Complex.mk z.re) (Set.uIcc z₁.im z.im) (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry)
|
||||
intro w hw
|
||||
constructor
|
||||
· simp
|
||||
calc dist z.re z₀.re
|
||||
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle z.re z₁.re z₀.re
|
||||
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
|
||||
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
|
||||
_ = rx := by
|
||||
rw [dist_comm]
|
||||
simp
|
||||
· simp
|
||||
calc dist w z₀.im
|
||||
_ ≤ dist w z₁.im + dist z₁.im z₀.im := by exact dist_triangle w z₁.im z₀.im
|
||||
_ ≤ dist z.im z₁.im + dist z₁.im z₀.im := by
|
||||
apply (add_le_add_iff_right (dist z₁.im z₀.im)).mpr
|
||||
rw [Set.uIcc_comm] at hw
|
||||
exact Real.dist_right_le_of_mem_uIcc hw
|
||||
_ < (ry - dist z₀.im z₁.im) + dist z₁.im z₀.im := by
|
||||
apply (add_lt_add_iff_right (dist z₁.im z₀.im)).mpr
|
||||
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).2
|
||||
_ = ry := by
|
||||
rw [dist_comm]
|
||||
simp
|
||||
rw [this]
|
||||
|
||||
simp
|
||||
|
||||
have {a b c d e f g h : E} : (a + b) + (c + d) - (e + f) - (g + h) = b + (a - g) - e - f + d - h + (c) := by
|
||||
abel
|
||||
rw [this]
|
||||
|
||||
|
||||
have H' : DifferentiableOn ℂ f (Set.uIcc z₁.re z.re ×ℂ Set.uIcc z₀.im z₁.im) := by
|
||||
apply DifferentiableOn.mono hf
|
||||
intro x hx
|
||||
constructor
|
||||
· simp
|
||||
calc dist x.re z₀.re
|
||||
_ ≤ dist x.re z₁.re + dist z₁.re z₀.re := by exact dist_triangle x.re z₁.re z₀.re
|
||||
_ ≤ dist z.re z₁.re + dist z₁.re z₀.re := by
|
||||
apply (add_le_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
rw [Set.uIcc_comm] at hx
|
||||
apply Real.dist_right_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).1
|
||||
_ < (rx - dist z₀.re z₁.re) + dist z₁.re z₀.re := by
|
||||
apply (add_lt_add_iff_right (dist z₁.re z₀.re)).mpr
|
||||
apply Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz).1
|
||||
_ = rx := by
|
||||
rw [dist_comm]
|
||||
simp
|
||||
· simp
|
||||
calc dist x.im z₀.im
|
||||
_ ≤ dist z₀.im z₁.im := by rw [dist_comm]; exact Real.dist_left_le_of_mem_uIcc (Complex.mem_reProdIm.1 hx).2
|
||||
_ < ry := by
|
||||
rw [dist_comm]
|
||||
exact Metric.mem_ball.1 (Complex.mem_reProdIm.1 hz₁).2
|
||||
|
||||
let A := Complex.integral_boundary_rect_eq_zero_of_differentiableOn f ⟨z₁.re, z₀.im⟩ ⟨z.re, z₁.im⟩ H'
|
||||
have {x : ℝ} {w : ℂ} : ↑x + w.im * Complex.I = { re := x, im := w.im } := by
|
||||
apply Complex.ext
|
||||
· simp
|
||||
· simp
|
||||
simp_rw [this] at A
|
||||
have {x : ℝ} {w : ℂ} : w.re + x * Complex.I = { re := w.re, im := x } := by
|
||||
apply Complex.ext
|
||||
· simp
|
||||
· simp
|
||||
simp_rw [this] at A
|
||||
rw [← A]
|
||||
abel
|
||||
|
||||
|
||||
theorem primitive_additivity'
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
{z₀ z₁ : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
(hz₁ : z₁ ∈ Metric.ball z₀ R)
|
||||
:
|
||||
primitive z₀ f =ᶠ[nhds z₁] fun z ↦ (primitive z₁ f z) + (primitive z₀ f z₁) := by
|
||||
|
||||
let d := fun ε ↦ √((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
|
||||
have h₀d : Continuous d := by continuity
|
||||
have h₁d : ∀ ε, 0 ≤ d ε := fun ε ↦ Real.sqrt_nonneg ((dist z₁.re z₀.re + ε) ^ 2 + (dist z₁.im z₀.im + ε) ^ 2)
|
||||
|
||||
obtain ⟨ε, h₀ε, h₁ε⟩ : ∃ ε > 0, d ε < R := by
|
||||
let Omega := d⁻¹' Metric.ball 0 R
|
||||
|
||||
have lem₀Ω : IsOpen Omega := IsOpen.preimage h₀d Metric.isOpen_ball
|
||||
have lem₁Ω : 0 ∈ Omega := by
|
||||
dsimp [Omega, d]; simp
|
||||
have : dist z₁.re z₀.re = |z₁.re - z₀.re| := by exact rfl
|
||||
rw [this]
|
||||
have : dist z₁.im z₀.im = |z₁.im - z₀.im| := by exact rfl
|
||||
rw [this]
|
||||
simp
|
||||
rw [← Complex.dist_eq_re_im]; simp
|
||||
exact hz₁
|
||||
obtain ⟨ε, h₁ε, h₂ε⟩ := Metric.isOpen_iff.1 lem₀Ω 0 lem₁Ω
|
||||
|
||||
let ε' := (2 : ℝ)⁻¹ * ε
|
||||
|
||||
have h₀ε' : ε' ∈ Omega := by
|
||||
apply h₂ε
|
||||
dsimp [ε']; simp
|
||||
have : |ε| = ε := by apply abs_of_pos h₁ε
|
||||
rw [this]
|
||||
apply (inv_mul_lt_iff zero_lt_two).mpr
|
||||
linarith
|
||||
have h₁ε' : 0 < ε' := by
|
||||
apply mul_pos _ h₁ε
|
||||
apply inv_pos.mpr
|
||||
exact zero_lt_two
|
||||
|
||||
use ε'
|
||||
|
||||
constructor
|
||||
· exact h₁ε'
|
||||
· dsimp [Omega] at h₀ε'; simp at h₀ε'
|
||||
rwa [abs_of_nonneg (h₁d ε')] at h₀ε'
|
||||
|
||||
let rx := dist z₁.re z₀.re + ε
|
||||
let ry := dist z₁.im z₀.im + ε
|
||||
|
||||
have h'ry : 0 < ry := by
|
||||
dsimp [ry]
|
||||
apply add_pos_of_nonneg_of_pos
|
||||
exact dist_nonneg
|
||||
simpa
|
||||
|
||||
have h'f : DifferentiableOn ℂ f (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
|
||||
apply hf.mono
|
||||
intro x hx
|
||||
simp
|
||||
rw [Complex.dist_eq_re_im]
|
||||
|
||||
have t₀ : dist x.re z₀.re < rx := Metric.mem_ball.mp hx.1
|
||||
have t₁ : dist x.im z₀.im < ry := Metric.mem_ball.mp hx.2
|
||||
have t₂ : √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2) < √( rx ^ 2 + ry ^ 2) := by
|
||||
rw [Real.sqrt_lt_sqrt_iff]
|
||||
apply add_lt_add
|
||||
· rw [sq_lt_sq]
|
||||
dsimp [dist] at t₀
|
||||
nth_rw 2 [abs_of_nonneg]
|
||||
assumption
|
||||
apply add_nonneg dist_nonneg (le_of_lt h₀ε)
|
||||
· rw [sq_lt_sq]
|
||||
dsimp [dist] at t₁
|
||||
nth_rw 2 [abs_of_nonneg]
|
||||
assumption
|
||||
apply add_nonneg dist_nonneg (le_of_lt h₀ε)
|
||||
apply add_nonneg
|
||||
exact sq_nonneg (x.re - z₀.re)
|
||||
exact sq_nonneg (x.im - z₀.im)
|
||||
|
||||
calc √((x.re - z₀.re) ^ 2 + (x.im - z₀.im) ^ 2)
|
||||
_ < √( rx ^ 2 + ry ^ 2) := by
|
||||
exact t₂
|
||||
_ = d ε := by dsimp [d, rx, ry]
|
||||
_ < R := by exact h₁ε
|
||||
|
||||
have h'z₁ : z₁ ∈ (Metric.ball z₀.re rx ×ℂ Metric.ball z₀.im ry) := by
|
||||
dsimp [rx, ry]
|
||||
constructor
|
||||
· simp; exact h₀ε
|
||||
· simp; exact h₀ε
|
||||
|
||||
obtain ⟨εx, hεx, εy, hεy, hε⟩ := primitive_additivity h'f h'ry h'z₁
|
||||
|
||||
apply Filter.eventuallyEq_iff_exists_mem.2
|
||||
use (Metric.ball z₁.re εx ×ℂ Metric.ball z₁.im εy)
|
||||
constructor
|
||||
· apply IsOpen.mem_nhds
|
||||
apply IsOpen.reProdIm
|
||||
exact Metric.isOpen_ball
|
||||
exact Metric.isOpen_ball
|
||||
constructor
|
||||
· simpa
|
||||
· simpa
|
||||
· intro x hx
|
||||
simp
|
||||
rw [← sub_zero (primitive z₀ f x), ← hε x hx]
|
||||
abel
|
||||
|
||||
|
||||
theorem primitive_hasDerivAt
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
{z₀ z : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
(hz : z ∈ Metric.ball z₀ R) :
|
||||
HasDerivAt (primitive z₀ f) (f z) z := by
|
||||
|
||||
let A := primitive_additivity' hf hz
|
||||
rw [Filter.EventuallyEq.hasDerivAt_iff A]
|
||||
rw [← add_zero (f z)]
|
||||
apply HasDerivAt.add
|
||||
|
||||
let R' := R - dist z z₀
|
||||
have h₀R' : 0 < R' := by
|
||||
dsimp [R']
|
||||
simp
|
||||
exact hz
|
||||
have h₁R' : Metric.ball z R' ⊆ Metric.ball z₀ R := by
|
||||
intro x hx
|
||||
simp
|
||||
calc dist x z₀
|
||||
_ ≤ dist x z + dist z z₀ := dist_triangle x z z₀
|
||||
_ < R' + dist z z₀ := by
|
||||
refine add_lt_add_right ?bc (dist z z₀)
|
||||
exact hx
|
||||
_ = R := by
|
||||
dsimp [R']
|
||||
simp
|
||||
|
||||
apply primitive_hasDerivAtBasepoint
|
||||
exact h₀R'
|
||||
apply ContinuousOn.mono hf.continuousOn h₁R'
|
||||
apply hasDerivAt_const
|
||||
|
||||
|
||||
theorem primitive_differentiableOn
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
{z₀ : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
:
|
||||
DifferentiableOn ℂ (primitive z₀ f) (Metric.ball z₀ R) := by
|
||||
intro z hz
|
||||
apply DifferentiableAt.differentiableWithinAt
|
||||
exact (primitive_hasDerivAt hf hz).differentiableAt
|
||||
|
||||
|
||||
theorem primitive_hasFderivAt
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
(z₀ : ℂ)
|
||||
(R : ℝ)
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
:
|
||||
∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) ((ContinuousLinearMap.lsmul ℂ ℂ).flip (f z)) z := by
|
||||
intro z hz
|
||||
rw [hasFDerivAt_iff_hasDerivAt]
|
||||
simp
|
||||
apply primitive_hasDerivAt hf hz
|
||||
|
||||
|
||||
theorem primitive_hasFderivAt'
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
:
|
||||
∀ z ∈ Metric.ball z₀ R, HasFDerivAt (primitive z₀ f) (ContinuousLinearMap.lsmul ℂ ℂ (f z)) z := by
|
||||
intro z hz
|
||||
rw [hasFDerivAt_iff_hasDerivAt]
|
||||
simp
|
||||
exact primitive_hasDerivAt hf hz
|
||||
|
||||
|
||||
theorem primitive_fderiv
|
||||
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
|
||||
{f : ℂ → E}
|
||||
{z₀ : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
:
|
||||
∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = (ContinuousLinearMap.lsmul ℂ ℂ).flip (f z) := by
|
||||
intro z hz
|
||||
apply HasFDerivAt.fderiv
|
||||
exact primitive_hasFderivAt z₀ R hf z hz
|
||||
|
||||
|
||||
theorem primitive_fderiv'
|
||||
{f : ℂ → ℂ}
|
||||
{z₀ : ℂ}
|
||||
{R : ℝ}
|
||||
(hf : DifferentiableOn ℂ f (Metric.ball z₀ R))
|
||||
:
|
||||
∀ z ∈ Metric.ball z₀ R, (fderiv ℂ (primitive z₀ f) z) = ContinuousLinearMap.lsmul ℂ ℂ (f z) := by
|
||||
intro z hz
|
||||
apply HasFDerivAt.fderiv
|
||||
exact primitive_hasFderivAt' hf z hz
|
|
@ -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.analyticOn_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 : AnalyticOn ℂ 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 := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
|
||||
tauto
|
||||
|
||||
|
||||
theorem supportZeroSet
|
||||
{f : ℂ → ℂ}
|
||||
{U : Set ℂ}
|
||||
(hU : IsPreconnected U)
|
||||
(h₁f : AnalyticOn ℂ 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 : AnalyticOn ℂ 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 : AnalyticOn ℂ 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 : AnalyticOn ℂ 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 : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
|
||||
(n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
|
||||
∃ F : ℂ → ℂ, (AnalyticOn ℂ 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 := AnalyticOn.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
|
|
@ -85,11 +85,11 @@ theorem laplace_add_ContDiffOn
|
|||
have t₁ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₁) x := by
|
||||
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
|
||||
let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
|
||||
apply A₀.differentiableAt (Preorder.le_refl 1)
|
||||
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
have t₂ : DifferentiableAt ℝ (partialDeriv ℝ 1 f₂) x := by
|
||||
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
|
||||
let A₀ := partialDeriv_contDiffAt ℝ B₀ 1
|
||||
exact A₀.differentiableAt (Preorder.le_refl 1)
|
||||
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
rw [partialDeriv_add₂_differentiableAt ℝ t₁ t₂]
|
||||
|
||||
have : partialDeriv ℝ Complex.I (f₁ + f₂) =ᶠ[nhds x] (partialDeriv ℝ Complex.I f₁) + (partialDeriv ℝ Complex.I f₂) := by
|
||||
|
@ -105,11 +105,11 @@ theorem laplace_add_ContDiffOn
|
|||
have t₃ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₁) x := by
|
||||
let B₀ := (h₁ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
|
||||
let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
|
||||
exact A₀.differentiableAt (Preorder.le_refl 1)
|
||||
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
have t₄ : DifferentiableAt ℝ (partialDeriv ℝ Complex.I f₂) x := by
|
||||
let B₀ := (h₂ x hx).contDiffAt (IsOpen.mem_nhds hs hx)
|
||||
let A₀ := partialDeriv_contDiffAt ℝ B₀ Complex.I
|
||||
exact A₀.differentiableAt (Preorder.le_refl 1)
|
||||
exact A₀.differentiableAt (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
rw [partialDeriv_add₂_differentiableAt ℝ t₃ t₄]
|
||||
|
||||
-- I am super confused at this point because the tactic 'ring' does not work.
|
||||
|
|
|
@ -4,12 +4,21 @@ 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
|
||||
import Mathlib.LinearAlgebra.Basis
|
||||
import Mathlib.LinearAlgebra.Contraction
|
||||
|
||||
open BigOperators
|
||||
open Finset
|
||||
|
||||
lemma OrthonormalBasis.sum_repr'
|
||||
{𝕜 : Type*} [RCLike 𝕜]
|
||||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
|
||||
[Fintype ι]
|
||||
(b : OrthonormalBasis ι 𝕜 E)
|
||||
(v : E) :
|
||||
v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
|
||||
nth_rw 1 [← (b.sum_repr v)]
|
||||
simp_rw [b.repr_apply_apply v]
|
||||
|
||||
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
|
||||
|
||||
|
|
|
@ -1,35 +0,0 @@
|
|||
import Mathlib.Analysis.Calculus.ContDiff.Basic
|
||||
import Mathlib.Analysis.Calculus.FDeriv.Add
|
||||
|
||||
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
|
||||
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
|
||||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
|
||||
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
|
||||
variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
|
||||
variable {f f₀ f₁ g : E → F}
|
||||
variable {f' f₀' f₁' g' : E →L[𝕜] F}
|
||||
variable (e : E →L[𝕜] F)
|
||||
variable {x : E}
|
||||
variable {s t : Set E}
|
||||
variable {L L₁ L₂ : Filter E}
|
||||
|
||||
variable {R : Type*} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F]
|
||||
|
||||
|
||||
-- import Mathlib.Analysis.Calculus.FDeriv.Add
|
||||
|
||||
@[fun_prop]
|
||||
theorem Differentiable.const_smul' (h : Differentiable 𝕜 f) (c : R) :
|
||||
Differentiable 𝕜 (c • f) := by
|
||||
have : c • f = fun x ↦ c • f x := rfl
|
||||
rw [this]
|
||||
exact Differentiable.const_smul h c
|
||||
|
||||
|
||||
-- Mathlib.Analysis.Calculus.ContDiff.Basic
|
||||
|
||||
theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
|
||||
ContDiff 𝕜 n (c • f) := by
|
||||
have : c • f = fun x ↦ c • f x := rfl
|
||||
rw [this]
|
||||
exact ContDiff.const_smul c hf
|
|
@ -38,18 +38,12 @@ theorem partialDeriv_eventuallyEq
|
|||
exact fun v => rfl
|
||||
|
||||
|
||||
theorem partialDeriv_smul₁
|
||||
{f : E → F}
|
||||
{a : 𝕜}
|
||||
{v : E} :
|
||||
partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
|
||||
theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
|
||||
unfold partialDeriv
|
||||
conv =>
|
||||
left
|
||||
intro w
|
||||
rw [map_smul]
|
||||
funext w
|
||||
simp
|
||||
|
||||
|
||||
theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by
|
||||
|
@ -58,8 +52,6 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v
|
|||
left
|
||||
intro w
|
||||
rw [map_add]
|
||||
funext w
|
||||
simp
|
||||
|
||||
|
||||
theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
|
||||
|
@ -78,7 +70,7 @@ theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv
|
|||
let ZZ := DifferentiableAt.const_smul contra a⁻¹
|
||||
have : (fun y => a⁻¹ • a • f y) = f := by
|
||||
funext i
|
||||
rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha]
|
||||
rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel ha]
|
||||
simp
|
||||
rw [this] at ZZ
|
||||
exact hf ZZ
|
||||
|
@ -98,8 +90,6 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f
|
|||
intro w
|
||||
left
|
||||
rw [fderiv_add (h₁ w) (h₂ w)]
|
||||
funext w
|
||||
simp
|
||||
|
||||
|
||||
theorem partialDeriv_add₂_differentiableAt
|
||||
|
@ -139,57 +129,6 @@ theorem partialDeriv_add₂_contDiffAt
|
|||
exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
|
||||
|
||||
|
||||
theorem partialDeriv_sub₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f₁) (h₂ : Differentiable 𝕜 f₂) : ∀ v : E, partialDeriv 𝕜 v (f₁ - f₂) = (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
|
||||
unfold partialDeriv
|
||||
intro v
|
||||
have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
|
||||
rw [this]
|
||||
conv =>
|
||||
left
|
||||
intro w
|
||||
left
|
||||
rw [fderiv_sub (h₁ w) (h₂ w)]
|
||||
funext w
|
||||
simp
|
||||
|
||||
|
||||
theorem partialDeriv_sub₂_differentiableAt
|
||||
{f₁ f₂ : E → F}
|
||||
{v : E}
|
||||
{x : E}
|
||||
(h₁ : DifferentiableAt 𝕜 f₁ x)
|
||||
(h₂ : DifferentiableAt 𝕜 f₂ x) :
|
||||
partialDeriv 𝕜 v (f₁ - f₂) x = (partialDeriv 𝕜 v f₁) x - (partialDeriv 𝕜 v f₂) x := by
|
||||
|
||||
unfold partialDeriv
|
||||
have : f₁ - f₂ = fun y ↦ f₁ y - f₂ y := by rfl
|
||||
rw [this]
|
||||
rw [fderiv_sub h₁ h₂]
|
||||
rfl
|
||||
|
||||
|
||||
theorem partialDeriv_sub₂_contDiffAt
|
||||
{f₁ f₂ : E → F}
|
||||
{v : E}
|
||||
{x : E}
|
||||
(h₁ : ContDiffAt 𝕜 1 f₁ x)
|
||||
(h₂ : ContDiffAt 𝕜 1 f₂ x) :
|
||||
partialDeriv 𝕜 v (f₁ - f₂) =ᶠ[nhds x] (partialDeriv 𝕜 v f₁) - (partialDeriv 𝕜 v f₂) := by
|
||||
|
||||
obtain ⟨f₁', u₁, hu₁, _, hf₁'⟩ := contDiffAt_one_iff.1 h₁
|
||||
obtain ⟨f₂', u₂, hu₂, _, hf₂'⟩ := contDiffAt_one_iff.1 h₂
|
||||
|
||||
apply Filter.eventuallyEq_iff_exists_mem.2
|
||||
use u₁ ∩ u₂
|
||||
constructor
|
||||
· exact Filter.inter_mem hu₁ hu₂
|
||||
· intro x hx
|
||||
simp
|
||||
apply partialDeriv_sub₂_differentiableAt 𝕜
|
||||
exact (hf₁' x (Set.mem_of_mem_inter_left hx)).differentiableAt
|
||||
exact (hf₂' x (Set.mem_of_mem_inter_right hx)).differentiableAt
|
||||
|
||||
|
||||
theorem partialDeriv_compContLin
|
||||
{f : E → F}
|
||||
{l : F →L[𝕜] G}
|
||||
|
@ -297,7 +236,7 @@ lemma partialDeriv_fderivOn
|
|||
rw [fderiv_clm_apply]
|
||||
· simp
|
||||
· convert DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
|
||||
apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
|
||||
apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 hf).2
|
||||
· simp
|
||||
|
||||
|
@ -356,11 +295,11 @@ theorem partialDeriv_smul'₂
|
|||
left_inv := by
|
||||
intro x
|
||||
simp
|
||||
rw [← smul_assoc, smul_eq_mul, mul_comm, mul_inv_cancel₀ ha, one_smul]
|
||||
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]
|
||||
rw [← smul_assoc, smul_eq_mul, mul_inv_cancel ha, one_smul]
|
||||
continuous_toFun := continuous_const_smul a
|
||||
continuous_invFun := continuous_const_smul a⁻¹
|
||||
}
|
||||
|
@ -407,7 +346,7 @@ theorem partialDeriv_comm
|
|||
let f'' := (fderiv ℝ f' z)
|
||||
have h₁ : HasFDerivAt f' f'' z := by
|
||||
apply DifferentiableAt.hasFDerivAt
|
||||
apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Preorder.le_refl 1)
|
||||
apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
|
||||
apply second_derivative_symmetric h₀ h₁ v₁ v₂
|
||||
|
||||
|
@ -441,7 +380,7 @@ theorem partialDeriv_commOn
|
|||
have h₁ : HasFDerivAt f' f'' z := by
|
||||
apply DifferentiableAt.hasFDerivAt
|
||||
apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
|
||||
apply ContDiffOn.differentiableOn _ (Preorder.le_refl 1)
|
||||
apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
|
||||
exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
|
||||
|
||||
have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by
|
||||
|
|
|
@ -1,101 +0,0 @@
|
|||
import Mathlib.MeasureTheory.Integral.Periodic
|
||||
|
||||
|
||||
theorem periodic_integrability₁
|
||||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f : ℝ → E}
|
||||
{t T : ℝ}
|
||||
{n : ℕ}
|
||||
(h₁f : Function.Periodic f T)
|
||||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||||
IntervalIntegrable f MeasureTheory.volume t (t + n * T) := by
|
||||
induction' n with n hn
|
||||
simp
|
||||
apply IntervalIntegrable.trans (b := t + n * T)
|
||||
exact hn
|
||||
|
||||
let A := IntervalIntegrable.comp_sub_right h₂f (n * T)
|
||||
have : f = fun x ↦ f (x - n * T) := by simp [Function.Periodic.sub_nat_mul_eq h₁f n]
|
||||
simp_rw [← this] at A
|
||||
have : (t + T + ↑n * T) = (t + ↑(n + 1) * T) := by simp; ring
|
||||
simp_rw [this] at A
|
||||
exact A
|
||||
|
||||
theorem periodic_integrability₂
|
||||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f : ℝ → E}
|
||||
{t T : ℝ}
|
||||
{n : ℕ}
|
||||
(h₁f : Function.Periodic f T)
|
||||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||||
IntervalIntegrable f MeasureTheory.volume (t - n * T) t := by
|
||||
induction' n with n hn
|
||||
simp
|
||||
--
|
||||
apply IntervalIntegrable.trans (b := t - n * T)
|
||||
--
|
||||
have A := IntervalIntegrable.comp_add_right h₂f (((n + 1): ℕ) * T)
|
||||
|
||||
have : f = fun x ↦ f (x + ((n + 1) : ℕ) * T) := by
|
||||
funext x
|
||||
have : x = x + ↑(n + 1) * T - ↑(n + 1) * T := by ring
|
||||
nth_rw 1 [this]
|
||||
rw [Function.Periodic.sub_nat_mul_eq h₁f]
|
||||
simp_rw [← this] at A
|
||||
have : (t + T - ↑(n + 1) * T) = (t - ↑n * T) := by simp; ring
|
||||
simp_rw [this] at A
|
||||
exact A
|
||||
--
|
||||
exact hn
|
||||
|
||||
|
||||
theorem periodic_integrability₃
|
||||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f : ℝ → E}
|
||||
{t T : ℝ}
|
||||
{n₁ n₂ : ℕ}
|
||||
(h₁f : Function.Periodic f T)
|
||||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||||
IntervalIntegrable f MeasureTheory.volume (t - n₁ * T) (t + n₂ * T) := by
|
||||
apply IntervalIntegrable.trans (b := t)
|
||||
exact periodic_integrability₂ h₁f h₂f
|
||||
exact periodic_integrability₁ h₁f h₂f
|
||||
|
||||
|
||||
theorem periodic_integrability4
|
||||
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f : ℝ → E}
|
||||
{t T : ℝ}
|
||||
{a₁ a₂ : ℝ}
|
||||
(h₁f : Function.Periodic f T)
|
||||
(hT : 0 < T)
|
||||
(h₂f : IntervalIntegrable f MeasureTheory.volume t (t + T)) :
|
||||
IntervalIntegrable f MeasureTheory.volume a₁ a₂ := by
|
||||
|
||||
obtain ⟨n₁, hn₁⟩ : ∃ n₁ : ℕ, t - n₁ * T ≤ min a₁ a₂ := by
|
||||
obtain ⟨n₁, hn₁⟩ := exists_nat_ge ((t -min a₁ a₂) / T)
|
||||
use n₁
|
||||
rw [sub_le_iff_le_add]
|
||||
rw [div_le_iff₀ hT] at hn₁
|
||||
rw [sub_le_iff_le_add] at hn₁
|
||||
rw [add_comm]
|
||||
exact hn₁
|
||||
obtain ⟨n₂, hn₂⟩ : ∃ n₂ : ℕ, max a₁ a₂ ≤ t + n₂ * T := by
|
||||
obtain ⟨n₂, hn₂⟩ := exists_nat_ge ((max a₁ a₂ - t) / T)
|
||||
use n₂
|
||||
rw [← sub_le_iff_le_add]
|
||||
rw [div_le_iff₀ hT] at hn₂
|
||||
linarith
|
||||
|
||||
have : Set.uIcc a₁ a₂ ⊆ Set.uIcc (t - n₁ * T) (t + n₂ * T) := by
|
||||
apply Set.uIcc_subset_uIcc_iff_le.mpr
|
||||
constructor
|
||||
· calc min (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||||
_ ≤ (t - ↑n₁ * T) := by exact min_le_left (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||||
_ ≤ min a₁ a₂ := by exact hn₁
|
||||
· calc max a₁ a₂
|
||||
_ ≤ t + n₂ * T := by exact hn₂
|
||||
_ ≤ max (t - ↑n₁ * T) (t + ↑n₂ * T) := by exact le_max_right (t - ↑n₁ * T) (t + ↑n₂ * T)
|
||||
|
||||
apply IntervalIntegrable.mono_set _ this
|
||||
exact periodic_integrability₃ h₁f h₂f
|
|
@ -0,0 +1,40 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
--import Mathlib.Analysis.Complex.Module
|
||||
|
||||
|
||||
|
||||
example simplificationTest₁
|
||||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E]
|
||||
{v : E}
|
||||
{z : ℂ} :
|
||||
z • v = z.re • v + Complex.I • z.im • v := by
|
||||
|
||||
/-
|
||||
An attempt to write "rw [add_smul]" will fail with "did not find instance of
|
||||
the pattern in the target -- expression (?r + ?s) • ?x".
|
||||
-/
|
||||
sorry
|
||||
|
||||
|
||||
theorem add_smul'
|
||||
(𝕜₁ : Type*) [NontriviallyNormedField ℝ]
|
||||
{𝕜₂ : Type*} [NontriviallyNormedField ℂ] [NormedAlgebra ℝ ℂ]
|
||||
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E]
|
||||
{v : E}
|
||||
{r s : ℂ} :
|
||||
(r + s) • v = r • v + s • v :=
|
||||
Module.add_smul r s v
|
||||
|
||||
|
||||
theorem smul_add' (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ :=
|
||||
DistribSMul.smul_add _ _ _
|
||||
#align smul_add smul_add
|
||||
|
||||
|
||||
|
||||
|
||||
example simplificationTest₂
|
||||
{v : E}
|
||||
{z : ℂ} :
|
||||
z • v = z.re • v + Complex.I • z.im • v := by
|
||||
sorry
|
|
@ -1,384 +0,0 @@
|
|||
import Mathlib.MeasureTheory.Integral.Periodic
|
||||
import Mathlib.MeasureTheory.Integral.CircleIntegral
|
||||
import Nevanlinna.specialFunctions_Integral_log_sin
|
||||
import Nevanlinna.harmonicAt_examples
|
||||
import Nevanlinna.harmonicAt_meanValue
|
||||
import Nevanlinna.periodic_integrability
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
|
||||
-- Lemmas for the circleMap
|
||||
|
||||
lemma l₀ {x₁ x₂ : ℝ} : (circleMap 0 1 x₁) * (circleMap 0 1 x₂) = circleMap 0 1 (x₁+x₂) := by
|
||||
dsimp [circleMap]
|
||||
simp
|
||||
rw [add_mul, Complex.exp_add]
|
||||
|
||||
lemma l₁ {x : ℝ} : ‖circleMap 0 1 x‖ = 1 := by
|
||||
rw [Complex.norm_eq_abs, abs_circleMap_zero]
|
||||
simp
|
||||
|
||||
lemma l₂ {x : ℝ} : ‖(circleMap 0 1 x) - a‖ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
|
||||
calc ‖(circleMap 0 1 x) - a‖
|
||||
_ = 1 * ‖(circleMap 0 1 x) - a‖ := by
|
||||
exact Eq.symm (one_mul ‖circleMap 0 1 x - a‖)
|
||||
_ = ‖(circleMap 0 1 (-x))‖ * ‖(circleMap 0 1 x) - a‖ := by
|
||||
rw [l₁]
|
||||
_ = ‖(circleMap 0 1 (-x)) * ((circleMap 0 1 x) - a)‖ := by
|
||||
exact Eq.symm (NormedField.norm_mul' (circleMap 0 1 (-x)) (circleMap 0 1 x - a))
|
||||
_ = ‖(circleMap 0 1 (-x)) * (circleMap 0 1 x) - (circleMap 0 1 (-x)) * a‖ := by
|
||||
rw [mul_sub]
|
||||
_ = ‖(circleMap 0 1 0) - (circleMap 0 1 (-x)) * a‖ := by
|
||||
rw [l₀]
|
||||
simp
|
||||
_ = ‖1 - (circleMap 0 1 (-x)) * a‖ := by
|
||||
congr
|
||||
dsimp [circleMap]
|
||||
simp
|
||||
|
||||
|
||||
-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ < 1.
|
||||
|
||||
lemma int'₀
|
||||
{a : ℂ}
|
||||
(ha : a ∈ Metric.ball 0 1) :
|
||||
IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
|
||||
apply Continuous.intervalIntegrable
|
||||
apply Continuous.log
|
||||
fun_prop
|
||||
simp
|
||||
intro x
|
||||
by_contra h₁a
|
||||
rw [← h₁a] at ha
|
||||
simp at ha
|
||||
|
||||
|
||||
lemma int₀
|
||||
{a : ℂ}
|
||||
(ha : a ∈ Metric.ball 0 1) :
|
||||
∫ (x : ℝ) in (0)..2 * π, log ‖circleMap 0 1 x - a‖ = 0 := by
|
||||
|
||||
by_cases h₁a : a = 0
|
||||
· -- case: a = 0
|
||||
rw [h₁a]
|
||||
simp
|
||||
|
||||
-- case: a ≠ 0
|
||||
simp_rw [l₂]
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
|
||||
conv =>
|
||||
left
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
|
||||
|
||||
let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
|
||||
dsimp [f₁]
|
||||
congr 4
|
||||
let A := periodic_circleMap 0 1 x
|
||||
simp at A
|
||||
exact id (Eq.symm A)
|
||||
conv =>
|
||||
left
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
|
||||
simp
|
||||
dsimp [f₁]
|
||||
|
||||
let ρ := ‖a‖⁻¹
|
||||
have hρ : 1 < ρ := by
|
||||
apply one_lt_inv_iff.mpr
|
||||
constructor
|
||||
· exact norm_pos_iff'.mpr h₁a
|
||||
· exact mem_ball_zero_iff.mp ha
|
||||
|
||||
let F := fun z ↦ log ‖1 - z * a‖
|
||||
|
||||
have hf : ∀ x ∈ Metric.ball 0 ρ, HarmonicAt F x := by
|
||||
intro x hx
|
||||
apply logabs_of_holomorphicAt_is_harmonic
|
||||
apply Differentiable.holomorphicAt
|
||||
fun_prop
|
||||
apply sub_ne_zero_of_ne
|
||||
by_contra h
|
||||
have : ‖x * a‖ < 1 := by
|
||||
calc ‖x * a‖
|
||||
_ = ‖x‖ * ‖a‖ := by exact NormedField.norm_mul' x a
|
||||
_ < ρ * ‖a‖ := by
|
||||
apply (mul_lt_mul_right _).2
|
||||
exact mem_ball_zero_iff.mp hx
|
||||
exact norm_pos_iff'.mpr h₁a
|
||||
_ = 1 := by
|
||||
dsimp [ρ]
|
||||
apply inv_mul_cancel₀
|
||||
exact (AbsoluteValue.ne_zero_iff Complex.abs).mpr h₁a
|
||||
rw [← h] at this
|
||||
simp at this
|
||||
|
||||
let A := harmonic_meanValue ρ 1 zero_lt_one hρ hf
|
||||
dsimp [F] at A
|
||||
simp at A
|
||||
exact A
|
||||
|
||||
|
||||
-- Integral of log ‖circleMap 0 1 x - 1‖
|
||||
|
||||
lemma int₁₁ : ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) = 0 := by
|
||||
|
||||
have t₁ {x : ℝ} : x ∈ Set.Ioo 0 π → log (4 * sin x ^ 2) = log 4 + 2 * log (sin x) := by
|
||||
intro hx
|
||||
rw [log_mul, log_pow]
|
||||
rfl
|
||||
exact Ne.symm (NeZero.ne' 4)
|
||||
apply pow_ne_zero 2
|
||||
apply (fun a => Ne.symm (ne_of_lt a))
|
||||
exact sin_pos_of_mem_Ioo hx
|
||||
|
||||
|
||||
have t₂ : Set.EqOn (fun y ↦ log (4 * sin y ^ 2)) (fun y ↦ log 4 + 2 * log (sin y)) (Set.Ioo 0 π) := by
|
||||
intro x hx
|
||||
simp
|
||||
rw [t₁ hx]
|
||||
|
||||
rw [intervalIntegral.integral_congr_volume pi_pos t₂]
|
||||
rw [intervalIntegral.integral_add]
|
||||
rw [intervalIntegral.integral_const_mul]
|
||||
simp
|
||||
rw [integral_log_sin₂]
|
||||
have : (4 : ℝ) = 2 * 2 := by norm_num
|
||||
rw [this, log_mul]
|
||||
ring
|
||||
norm_num
|
||||
norm_num
|
||||
-- IntervalIntegrable (fun x => log 4) volume 0 π
|
||||
simp
|
||||
-- IntervalIntegrable (fun x => 2 * log (sin x)) volume 0 π
|
||||
apply IntervalIntegrable.const_mul
|
||||
exact intervalIntegrable_log_sin
|
||||
|
||||
lemma logAffineHelper {x : ℝ} : log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2 := by
|
||||
dsimp [Complex.abs]
|
||||
rw [log_sqrt (Complex.normSq_nonneg (circleMap 0 1 x - 1))]
|
||||
congr
|
||||
calc Complex.normSq (circleMap 0 1 x - 1)
|
||||
_ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
|
||||
dsimp [circleMap]
|
||||
rw [Complex.normSq_apply]
|
||||
simp
|
||||
_ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
|
||||
ring
|
||||
_ = 2 - 2 * cos x := by
|
||||
rw [sin_sq_add_cos_sq]
|
||||
norm_num
|
||||
_ = 2 - 2 * cos (2 * (x / 2)) := by
|
||||
rw [← mul_div_assoc]
|
||||
congr; norm_num
|
||||
_ = 4 - 4 * cos (x / 2) ^ 2 := by
|
||||
rw [cos_two_mul]
|
||||
ring
|
||||
_ = 4 * sin (x / 2) ^ 2 := by
|
||||
nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
|
||||
ring
|
||||
|
||||
lemma int'₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖
|
||||
IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume 0 (2 * π) := by
|
||||
|
||||
simp_rw [logAffineHelper]
|
||||
apply IntervalIntegrable.div_const
|
||||
rw [← IntervalIntegrable.comp_mul_left_iff (c := 2) (Ne.symm (NeZero.ne' 2))]
|
||||
simp
|
||||
|
||||
have h₁ : Set.EqOn (fun x => log (4 * sin x ^ 2)) (fun x => log 4 + 2 * log (sin x)) (Set.Ioo 0 π) := by
|
||||
intro x hx
|
||||
simp [log_mul (Ne.symm (NeZero.ne' 4)), log_pow, ne_of_gt (sin_pos_of_mem_Ioo hx)]
|
||||
rw [IntervalIntegrable.integral_congr_Ioo pi_nonneg h₁]
|
||||
apply IntervalIntegrable.add
|
||||
simp
|
||||
apply IntervalIntegrable.const_mul
|
||||
exact intervalIntegrable_log_sin
|
||||
|
||||
lemma int''₁ : -- Integrability of log ‖circleMap 0 1 x - 1‖ for arbitrary intervals
|
||||
∀ (t₁ t₂ : ℝ), IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - 1‖) volume t₁ t₂ := by
|
||||
intro t₁ t₂
|
||||
|
||||
apply periodic_integrability4 (T := 2 * π) (t := 0)
|
||||
--
|
||||
have : (fun x => log ‖circleMap 0 1 x - 1‖) = (fun x => log ‖x - 1‖) ∘ (circleMap 0 1) := rfl
|
||||
rw [this]
|
||||
apply Function.Periodic.comp
|
||||
exact periodic_circleMap 0 1
|
||||
--
|
||||
exact two_pi_pos
|
||||
--
|
||||
rw [zero_add]
|
||||
exact int'₁
|
||||
|
||||
lemma int₁ :
|
||||
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - 1‖ = 0 := by
|
||||
|
||||
simp_rw [logAffineHelper]
|
||||
simp
|
||||
|
||||
have : ∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2) = 2 * ∫ (x : ℝ) in (0)..π, log (4 * sin x ^ 2) := by
|
||||
have : 1 = 2 * (2 : ℝ)⁻¹ := by exact Eq.symm (mul_inv_cancel_of_invertible 2)
|
||||
nth_rw 1 [← one_mul (∫ (x : ℝ) in (0)..2 * π, log (4 * sin (x / 2) ^ 2))]
|
||||
rw [← mul_inv_cancel_of_invertible 2, mul_assoc]
|
||||
let f := fun y ↦ log (4 * sin y ^ 2)
|
||||
have {x : ℝ} : log (4 * sin (x / 2) ^ 2) = f (x / 2) := by simp
|
||||
conv =>
|
||||
left
|
||||
right
|
||||
right
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [intervalIntegral.inv_mul_integral_comp_div 2]
|
||||
simp
|
||||
rw [this]
|
||||
simp
|
||||
exact int₁₁
|
||||
|
||||
|
||||
-- Integral of log ‖circleMap 0 1 x - a‖, for ‖a‖ = 1
|
||||
|
||||
lemma int'₂
|
||||
{a : ℂ}
|
||||
(ha : ‖a‖ = 1) :
|
||||
IntervalIntegrable (fun x ↦ log ‖circleMap 0 1 x - a‖) volume 0 (2 * π) := by
|
||||
|
||||
simp_rw [l₂]
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
|
||||
conv =>
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [IntervalIntegrable.iff_comp_neg]
|
||||
|
||||
let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
|
||||
dsimp [f₁]
|
||||
congr 4
|
||||
let A := periodic_circleMap 0 1 x
|
||||
simp at A
|
||||
exact id (Eq.symm A)
|
||||
conv =>
|
||||
arg 1
|
||||
intro x
|
||||
arg 0
|
||||
intro w
|
||||
rw [this]
|
||||
simp
|
||||
have : 0 = 2 * π - 2 * π := by ring
|
||||
rw [this]
|
||||
have : -(2 * π ) = 0 - 2 * π := by ring
|
||||
rw [this]
|
||||
apply IntervalIntegrable.comp_add_right _ (2 * π) --f₁ (2 * π)
|
||||
dsimp [f₁]
|
||||
|
||||
have : ∃ ζ, a = circleMap 0 1 ζ := by
|
||||
apply Set.exists_range_iff.mp
|
||||
use a
|
||||
simp
|
||||
exact ha
|
||||
obtain ⟨ζ, hζ⟩ := this
|
||||
rw [hζ]
|
||||
simp_rw [l₀]
|
||||
|
||||
have : 2 * π = (2 * π + ζ) - ζ := by ring
|
||||
rw [this]
|
||||
have : 0 = ζ - ζ := by ring
|
||||
rw [this]
|
||||
have : (fun w => log (Complex.abs (1 - circleMap 0 1 (w + ζ)))) = fun x ↦ (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w)))) (x + ζ) := rfl
|
||||
rw [this]
|
||||
apply IntervalIntegrable.comp_add_right (f := (fun w ↦ log (Complex.abs (1 - circleMap 0 1 (w))))) _ ζ
|
||||
|
||||
have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
|
||||
have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
|
||||
rw [this]
|
||||
apply Function.Periodic.comp
|
||||
exact periodic_circleMap 0 1
|
||||
|
||||
let A := int''₁ (2 * π + ζ) ζ
|
||||
have {x : ℝ} : ‖circleMap 0 1 x - 1‖ = Complex.abs (1 - circleMap 0 1 x) := AbsoluteValue.map_sub Complex.abs (circleMap 0 1 x) 1
|
||||
simp_rw [this] at A
|
||||
exact A
|
||||
|
||||
|
||||
lemma int₂
|
||||
{a : ℂ}
|
||||
(ha : ‖a‖ = 1) :
|
||||
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
|
||||
|
||||
simp_rw [l₂]
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 (-x) * a‖ = (fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖) (-x) := by rfl
|
||||
conv =>
|
||||
left
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [intervalIntegral.integral_comp_neg ((fun w ↦ log ‖1 - circleMap 0 1 (w) * a‖))]
|
||||
|
||||
let f₁ := fun w ↦ log ‖1 - circleMap 0 1 w * a‖
|
||||
have {x : ℝ} : log ‖1 - circleMap 0 1 x * a‖ = f₁ (x + 2 * π) := by
|
||||
dsimp [f₁]
|
||||
congr 4
|
||||
let A := periodic_circleMap 0 1 x
|
||||
simp at A
|
||||
exact id (Eq.symm A)
|
||||
conv =>
|
||||
left
|
||||
arg 1
|
||||
intro x
|
||||
rw [this]
|
||||
rw [intervalIntegral.integral_comp_add_right f₁ (2 * π)]
|
||||
simp
|
||||
dsimp [f₁]
|
||||
|
||||
have : ∃ ζ, a = circleMap 0 1 ζ := by
|
||||
apply Set.exists_range_iff.mp
|
||||
use a
|
||||
simp
|
||||
exact ha
|
||||
obtain ⟨ζ, hζ⟩ := this
|
||||
rw [hζ]
|
||||
simp_rw [l₀]
|
||||
|
||||
rw [intervalIntegral.integral_comp_add_right (f := fun x ↦ log (Complex.abs (1 - circleMap 0 1 (x))))]
|
||||
|
||||
have : Function.Periodic (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) (2 * π) := by
|
||||
have : (fun x ↦ log (Complex.abs (1 - circleMap 0 1 x))) = ( (fun x ↦ log (Complex.abs (1 - x))) ∘ (circleMap 0 1) ) := by rfl
|
||||
rw [this]
|
||||
apply Function.Periodic.comp
|
||||
exact periodic_circleMap 0 1
|
||||
|
||||
let A := Function.Periodic.intervalIntegral_add_eq this ζ 0
|
||||
simp at A
|
||||
simp
|
||||
rw [add_comm]
|
||||
rw [A]
|
||||
|
||||
have {x : ℝ} : log (Complex.abs (1 - circleMap 0 1 x)) = log ‖circleMap 0 1 x - 1‖ := by
|
||||
rw [← AbsoluteValue.map_neg Complex.abs]
|
||||
simp
|
||||
simp_rw [this]
|
||||
exact int₁
|
||||
|
||||
|
||||
lemma int₃
|
||||
{a : ℂ}
|
||||
(ha : a ∈ Metric.closedBall 0 1) :
|
||||
∫ x in (0)..(2 * π), log ‖circleMap 0 1 x - a‖ = 0 := by
|
||||
by_cases h₁a : a ∈ Metric.ball 0 1
|
||||
· exact int₀ h₁a
|
||||
· apply int₂
|
||||
simp at ha
|
||||
simp at h₁a
|
||||
simp
|
||||
linarith
|
|
@ -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]
|
|
@ -1,374 +0,0 @@
|
|||
import Mathlib.Analysis.SpecialFunctions.Integrals
|
||||
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
|
||||
import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
|
||||
|
||||
open scoped Interval Topology
|
||||
open Real Filter MeasureTheory intervalIntegral
|
||||
|
||||
|
||||
|
||||
lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((π / 2)⁻¹ * x)‖ := by
|
||||
|
||||
intro x hx
|
||||
by_cases h'x : x = 0
|
||||
· rw [h'x]; simp
|
||||
|
||||
-- Now handle the case where x ≠ 0
|
||||
have l₀ : log ((π / 2)⁻¹ * x) ≤ 0 := by
|
||||
apply log_nonpos
|
||||
apply mul_nonneg
|
||||
apply le_of_lt
|
||||
apply inv_pos.2
|
||||
apply div_pos
|
||||
exact pi_pos
|
||||
exact zero_lt_two
|
||||
apply (Set.mem_Icc.1 hx).1
|
||||
simp
|
||||
apply mul_le_one
|
||||
rw [div_le_one pi_pos]
|
||||
exact two_le_pi
|
||||
exact (Set.mem_Icc.1 hx).1
|
||||
exact (Set.mem_Icc.1 hx).2
|
||||
|
||||
have l₁ : 0 ≤ sin x := by
|
||||
apply sin_nonneg_of_nonneg_of_le_pi (Set.mem_Icc.1 hx).1
|
||||
trans (1 : ℝ)
|
||||
exact (Set.mem_Icc.1 hx).2
|
||||
trans π / 2
|
||||
exact one_le_pi_div_two
|
||||
norm_num [pi_nonneg]
|
||||
have l₂ : log (sin x) ≤ 0 := log_nonpos l₁ (sin_le_one x)
|
||||
|
||||
simp only [norm_eq_abs, Function.comp_apply]
|
||||
rw [abs_eq_neg_self.2 l₀]
|
||||
rw [abs_eq_neg_self.2 l₂]
|
||||
simp only [neg_le_neg_iff, ge_iff_le]
|
||||
|
||||
have l₃ : x ∈ (Set.Ioi 0) := by
|
||||
simp
|
||||
exact lt_of_le_of_ne (Set.mem_Icc.1 hx).1 ( fun a => h'x (id (Eq.symm a)) )
|
||||
|
||||
have l₅ : 0 < (π / 2)⁻¹ * x := by
|
||||
apply mul_pos
|
||||
apply inv_pos.2
|
||||
apply div_pos pi_pos zero_lt_two
|
||||
exact l₃
|
||||
|
||||
have : ∀ x ∈ (Set.Icc 0 (π / 2)), (π / 2)⁻¹ * x ≤ sin x := by
|
||||
intro x hx
|
||||
|
||||
have i₀ : 0 ∈ Set.Icc 0 π :=
|
||||
Set.left_mem_Icc.mpr pi_nonneg
|
||||
have i₁ : π / 2 ∈ Set.Icc 0 π :=
|
||||
Set.mem_Icc.mpr ⟨div_nonneg pi_nonneg zero_le_two, half_le_self pi_nonneg⟩
|
||||
|
||||
have i₂ : 0 ≤ 1 - (π / 2)⁻¹ * x := by
|
||||
rw [sub_nonneg]
|
||||
calc (π / 2)⁻¹ * x
|
||||
_ ≤ (π / 2)⁻¹ * (π / 2) := by
|
||||
apply mul_le_mul_of_nonneg_left
|
||||
exact (Set.mem_Icc.1 hx).2
|
||||
apply inv_nonneg.mpr (div_nonneg pi_nonneg zero_le_two)
|
||||
_ = 1 := by
|
||||
apply inv_mul_cancel₀
|
||||
apply div_ne_zero_iff.mpr
|
||||
constructor
|
||||
· exact pi_ne_zero
|
||||
· exact Ne.symm (NeZero.ne' 2)
|
||||
|
||||
have i₃ : 0 ≤ (π / 2)⁻¹ * x := by
|
||||
apply mul_nonneg
|
||||
apply inv_nonneg.2
|
||||
apply div_nonneg
|
||||
exact pi_nonneg
|
||||
exact zero_le_two
|
||||
exact (Set.mem_Icc.1 hx).1
|
||||
|
||||
have i₄ : 1 - (π / 2)⁻¹ * x + (π / 2)⁻¹ * x = 1 := by ring
|
||||
|
||||
let B := strictConcaveOn_sin_Icc.concaveOn.2 i₀ i₁ i₂ i₃ i₄
|
||||
simp [Real.sin_pi_div_two] at B
|
||||
rw [(by ring_nf; rw [mul_inv_cancel₀ pi_ne_zero, one_mul] : 2 / π * x * (π / 2) = x)] at B
|
||||
simpa
|
||||
|
||||
apply log_le_log l₅
|
||||
apply this
|
||||
apply Set.mem_Icc.mpr
|
||||
constructor
|
||||
· exact le_of_lt l₃
|
||||
· trans 1
|
||||
exact (Set.mem_Icc.1 hx).2
|
||||
exact one_le_pi_div_two
|
||||
|
||||
|
||||
lemma intervalIntegrable_log_sin₁ : IntervalIntegrable (log ∘ sin) volume 0 1 := by
|
||||
|
||||
have int_log : IntervalIntegrable (fun x ↦ ‖log x‖) volume 0 1 := by
|
||||
apply IntervalIntegrable.norm
|
||||
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 int_log : IntervalIntegrable (fun x ↦ ‖log ((π / 2)⁻¹ * x)‖) volume 0 1 := by
|
||||
|
||||
have A := IntervalIntegrable.comp_mul_right int_log (π / 2)⁻¹
|
||||
simp only [norm_eq_abs] at A
|
||||
conv =>
|
||||
arg 1
|
||||
intro x
|
||||
rw [mul_comm]
|
||||
simp only [norm_eq_abs]
|
||||
apply IntervalIntegrable.mono A
|
||||
simp
|
||||
trans Set.Icc 0 (π / 2)
|
||||
exact Set.Icc_subset_Icc (Preorder.le_refl 0) one_le_pi_div_two
|
||||
exact Set.Icc_subset_uIcc
|
||||
exact Preorder.le_refl volume
|
||||
|
||||
apply IntervalIntegrable.mono_fun' (g := fun x ↦ ‖log ((π / 2)⁻¹ * x)‖)
|
||||
exact int_log
|
||||
|
||||
-- AEStronglyMeasurable (log ∘ sin) (volume.restrict (Ι 0 1))
|
||||
apply ContinuousOn.aestronglyMeasurable
|
||||
apply ContinuousOn.comp (t := Ι 0 1)
|
||||
apply ContinuousOn.mono (s := {0}ᶜ)
|
||||
exact continuousOn_log
|
||||
intro x hx
|
||||
by_contra contra
|
||||
simp at contra
|
||||
rw [contra, Set.left_mem_uIoc] at hx
|
||||
linarith
|
||||
exact continuousOn_sin
|
||||
|
||||
-- Set.MapsTo sin (Ι 0 1) (Ι 0 1)
|
||||
rw [Set.uIoc_of_le (zero_le_one' ℝ)]
|
||||
exact fun x hx ↦ ⟨sin_pos_of_pos_of_le_one hx.1 hx.2, sin_le_one x⟩
|
||||
|
||||
-- MeasurableSet (Ι 0 1)
|
||||
exact measurableSet_uIoc
|
||||
|
||||
-- (fun x => ‖(log ∘ sin) x‖) ≤ᶠ[ae (volume.restrict (Ι 0 1))] ‖log‖
|
||||
dsimp [EventuallyLE]
|
||||
rw [MeasureTheory.ae_restrict_iff]
|
||||
apply MeasureTheory.ae_of_all
|
||||
intro x hx
|
||||
have : x ∈ Set.Icc 0 1 := by
|
||||
simp
|
||||
simp at hx
|
||||
constructor
|
||||
· exact le_of_lt hx.1
|
||||
· exact hx.2
|
||||
let A := logsinBound x this
|
||||
simp only [Function.comp_apply, norm_eq_abs] at A
|
||||
exact A
|
||||
|
||||
apply measurableSet_le
|
||||
apply Measurable.comp'
|
||||
exact continuous_abs.measurable
|
||||
exact Measurable.comp' measurable_log continuous_sin.measurable
|
||||
-- Measurable fun a => |log ((π / 2)⁻¹ * a)|
|
||||
apply Measurable.comp'
|
||||
exact continuous_abs.measurable
|
||||
apply Measurable.comp'
|
||||
exact measurable_log
|
||||
exact measurable_const_mul (π / 2)⁻¹
|
||||
|
||||
lemma intervalIntegrable_log_sin₂ : IntervalIntegrable (log ∘ sin) volume 0 (π / 2) := by
|
||||
|
||||
apply IntervalIntegrable.trans (b := 1)
|
||||
exact intervalIntegrable_log_sin₁
|
||||
|
||||
-- IntervalIntegrable (log ∘ sin) volume 1 (π / 2)
|
||||
apply ContinuousOn.intervalIntegrable
|
||||
apply ContinuousOn.comp continuousOn_log continuousOn_sin
|
||||
intro x hx
|
||||
rw [Set.uIcc_of_le, Set.mem_Icc] at hx
|
||||
have : 0 < sin x := by
|
||||
apply Real.sin_pos_of_pos_of_lt_pi
|
||||
· calc 0
|
||||
_ < 1 := Real.zero_lt_one
|
||||
_ ≤ x := hx.1
|
||||
· calc x
|
||||
_ ≤ π / 2 := hx.2
|
||||
_ < π := div_two_lt_of_pos pi_pos
|
||||
by_contra h₁x
|
||||
simp at h₁x
|
||||
rw [h₁x] at this
|
||||
simp at this
|
||||
exact one_le_pi_div_two
|
||||
|
||||
theorem intervalIntegrable_log_sin : IntervalIntegrable (log ∘ sin) volume 0 π := by
|
||||
apply IntervalIntegrable.trans (b := π / 2)
|
||||
exact intervalIntegrable_log_sin₂
|
||||
-- IntervalIntegrable (log ∘ sin) volume (π / 2) π
|
||||
let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ π
|
||||
simp at A
|
||||
let B := IntervalIntegrable.symm A
|
||||
have : π - π / 2 = π / 2 := by linarith
|
||||
rwa [this] at B
|
||||
|
||||
theorem intervalIntegrable_log_cos : IntervalIntegrable (log ∘ cos) volume 0 (π / 2) := by
|
||||
let A := IntervalIntegrable.comp_sub_left intervalIntegrable_log_sin₂ (π / 2)
|
||||
simp only [Function.comp_apply, sub_zero, sub_self] at A
|
||||
simp_rw [sin_pi_div_two_sub] at A
|
||||
have : (fun x => log (cos x)) = log ∘ cos := rfl
|
||||
apply IntervalIntegrable.symm
|
||||
rwa [← this]
|
||||
|
||||
|
||||
theorem intervalIntegral.integral_congr_volume
|
||||
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f : ℝ → E}
|
||||
{g : ℝ → E}
|
||||
{a : ℝ}
|
||||
{b : ℝ}
|
||||
(h₀ : a < b)
|
||||
(h₁ : Set.EqOn f g (Set.Ioo a b)) :
|
||||
∫ (x : ℝ) in a..b, f x = ∫ (x : ℝ) in a..b, g x := by
|
||||
|
||||
apply intervalIntegral.integral_congr_ae
|
||||
rw [MeasureTheory.ae_iff]
|
||||
apply nonpos_iff_eq_zero.1
|
||||
push_neg
|
||||
have : {x | x ∈ Ι a b ∧ f x ≠ g x} ⊆ {b} := by
|
||||
intro x hx
|
||||
have t₂ : x ∈ Ι a b \ Set.Ioo a b := by
|
||||
constructor
|
||||
· exact hx.1
|
||||
· by_contra H
|
||||
exact hx.2 (h₁ H)
|
||||
rw [Set.uIoc_of_le (le_of_lt h₀)] at t₂
|
||||
rw [Set.Ioc_diff_Ioo_same h₀] at t₂
|
||||
assumption
|
||||
calc volume {a_1 | a_1 ∈ Ι a b ∧ f a_1 ≠ g a_1}
|
||||
_ ≤ volume {b} := volume.mono this
|
||||
_ = 0 := volume_singleton
|
||||
|
||||
|
||||
theorem IntervalIntegrable.integral_congr_Ioo
|
||||
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E]
|
||||
{f g : ℝ → E}
|
||||
{a b : ℝ}
|
||||
(hab : a ≤ b)
|
||||
(hfg : Set.EqOn f g (Set.Ioo a b)) :
|
||||
IntervalIntegrable f volume a b ↔ IntervalIntegrable g volume a b := by
|
||||
|
||||
rw [intervalIntegrable_iff_integrableOn_Ioo_of_le hab]
|
||||
rw [MeasureTheory.integrableOn_congr_fun hfg measurableSet_Ioo]
|
||||
rw [← intervalIntegrable_iff_integrableOn_Ioo_of_le hab]
|
||||
|
||||
|
||||
|
||||
lemma integral_log_sin₀ : ∫ (x : ℝ) in (0)..π, log (sin x) = 2 * ∫ (x : ℝ) in (0)..(π / 2), log (sin x) := by
|
||||
rw [← intervalIntegral.integral_add_adjacent_intervals (a := 0) (b := π / 2) (c := π)]
|
||||
conv =>
|
||||
left
|
||||
right
|
||||
arg 1
|
||||
intro x
|
||||
rw [← sin_pi_sub]
|
||||
rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) π]
|
||||
have : π - π / 2 = π / 2 := by linarith
|
||||
rw [this]
|
||||
simp
|
||||
ring
|
||||
-- IntervalIntegrable (fun x => log (sin x)) volume 0 (π / 2)
|
||||
exact intervalIntegrable_log_sin₂
|
||||
-- IntervalIntegrable (fun x => log (sin x)) volume (π / 2) π
|
||||
apply intervalIntegrable_log_sin.mono_set
|
||||
rw [Set.uIcc_of_le, Set.uIcc_of_le]
|
||||
apply Set.Icc_subset_Icc_left
|
||||
linarith [pi_pos]
|
||||
linarith [pi_pos]
|
||||
linarith [pi_pos]
|
||||
|
||||
|
||||
lemma integral_log_sin₁ : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = -log 2 * π/2 := by
|
||||
|
||||
have t₁ {x : ℝ} : x ∈ Set.Ioo 0 (π / 2) → log (sin (2 * x)) = log 2 + log (sin x) + log (cos x) := by
|
||||
intro hx
|
||||
simp at hx
|
||||
|
||||
rw [sin_two_mul x, log_mul, log_mul]
|
||||
exact Ne.symm (NeZero.ne' 2)
|
||||
-- sin x ≠ 0
|
||||
apply (fun a => Ne.symm (ne_of_lt a))
|
||||
apply sin_pos_of_mem_Ioo
|
||||
constructor
|
||||
· exact hx.1
|
||||
· linarith [pi_pos, hx.2]
|
||||
-- 2 * sin x ≠ 0
|
||||
simp
|
||||
apply (fun a => Ne.symm (ne_of_lt a))
|
||||
apply sin_pos_of_mem_Ioo
|
||||
constructor
|
||||
· exact hx.1
|
||||
· linarith [pi_pos, hx.2]
|
||||
-- cos x ≠ 0
|
||||
apply (fun a => Ne.symm (ne_of_lt a))
|
||||
apply cos_pos_of_mem_Ioo
|
||||
constructor
|
||||
· linarith [pi_pos, hx.1]
|
||||
· exact hx.2
|
||||
|
||||
have t₂ : Set.EqOn (fun y ↦ log (sin y)) (fun y ↦ log (sin (2 * y)) - log 2 - log (cos y)) (Set.Ioo 0 (π / 2)) := by
|
||||
intro x hx
|
||||
simp
|
||||
rw [t₁ hx]
|
||||
ring
|
||||
|
||||
rw [intervalIntegral.integral_congr_volume _ t₂]
|
||||
rw [intervalIntegral.integral_sub, intervalIntegral.integral_sub]
|
||||
rw [intervalIntegral.integral_const]
|
||||
rw [intervalIntegral.integral_comp_mul_left (c := 2) (f := fun x ↦ log (sin x))]
|
||||
simp
|
||||
have : 2 * (π / 2) = π := by linarith
|
||||
rw [this]
|
||||
rw [integral_log_sin₀]
|
||||
|
||||
have : ∫ (x : ℝ) in (0)..(π / 2), log (sin x) = ∫ (x : ℝ) in (0)..(π / 2), log (cos x) := by
|
||||
conv =>
|
||||
right
|
||||
arg 1
|
||||
intro x
|
||||
rw [← sin_pi_div_two_sub]
|
||||
rw [intervalIntegral.integral_comp_sub_left (fun x ↦ log (sin x)) (π / 2)]
|
||||
simp
|
||||
rw [← this]
|
||||
simp
|
||||
linarith
|
||||
|
||||
exact Ne.symm (NeZero.ne' 2)
|
||||
-- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
|
||||
let A := intervalIntegrable_log_sin.comp_mul_left 2
|
||||
simp at A
|
||||
assumption
|
||||
-- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
|
||||
simp
|
||||
-- IntervalIntegrable (fun x => log (sin (2 * x)) - log 2) volume 0 (π / 2)
|
||||
apply IntervalIntegrable.sub
|
||||
-- -- IntervalIntegrable (fun x => log (sin (2 * x))) volume 0 (π / 2)
|
||||
let A := intervalIntegrable_log_sin.comp_mul_left 2
|
||||
simp at A
|
||||
assumption
|
||||
-- -- IntervalIntegrable (fun x => log 2) volume 0 (π / 2)
|
||||
simp
|
||||
-- -- IntervalIntegrable (fun x => log (cos x)) volume 0 (π / 2)
|
||||
exact intervalIntegrable_log_cos
|
||||
--
|
||||
linarith [pi_pos]
|
||||
|
||||
|
||||
lemma integral_log_sin₂ : ∫ (x : ℝ) in (0)..π, log (sin x) = -log 2 * π := by
|
||||
rw [integral_log_sin₀, integral_log_sin₁]
|
||||
ring
|
|
@ -0,0 +1,47 @@
|
|||
import Mathlib.Analysis.InnerProductSpace.PiL2
|
||||
|
||||
|
||||
open RCLike Real Filter
|
||||
open Topology ComplexConjugate
|
||||
open LinearMap (BilinForm)
|
||||
open TensorProduct
|
||||
open InnerProductSpace
|
||||
open Inner
|
||||
|
||||
|
||||
example
|
||||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
|
||||
{F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
|
||||
: 1 = 0 := by
|
||||
|
||||
let e : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := innerₗ E
|
||||
let f : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₗ F
|
||||
let e₂ := TensorProduct.map₂ e f
|
||||
let l := TensorProduct.lid ℝ ℝ
|
||||
|
||||
have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) =
|
||||
|
||||
let X : InnerProductSpace.Core ℝ (E ⊗[ℝ] F) := {
|
||||
inner := by
|
||||
intro a b
|
||||
exact TensorProduct.lid ℝ ℝ ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
|
||||
conj_symm := by
|
||||
simp
|
||||
intro x y
|
||||
|
||||
unfold innerₗ
|
||||
|
||||
simp
|
||||
sorry
|
||||
nonneg_re := _
|
||||
definite := _
|
||||
add_left := _
|
||||
smul_left := _
|
||||
}
|
||||
|
||||
let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 :=
|
||||
--let x := TensorProduct.lift
|
||||
--E.inner
|
||||
--TensorProduct.map₂
|
||||
sorry
|
||||
sorry
|
|
@ -0,0 +1,130 @@
|
|||
import Mathlib.Analysis.Complex.CauchyIntegral
|
||||
--import Mathlib.Analysis.Complex.Module
|
||||
|
||||
|
||||
open ComplexConjugate
|
||||
|
||||
#check DiffContOnCl.circleIntegral_sub_inv_smul
|
||||
|
||||
open Real
|
||||
|
||||
theorem CauchyIntegralFormula :
|
||||
∀
|
||||
{R : ℝ} -- Radius of the ball
|
||||
{w : ℂ} -- Point in the interior of the ball
|
||||
{f : ℂ → ℂ}, -- Holomorphic function
|
||||
DiffContOnCl ℂ f (Metric.ball 0 R)
|
||||
→ w ∈ Metric.ball 0 R
|
||||
→ (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * π * Complex.I) • f w := by
|
||||
|
||||
exact DiffContOnCl.circleIntegral_sub_inv_smul
|
||||
|
||||
#check CauchyIntegralFormula
|
||||
#check HasDerivAt.continuousAt
|
||||
#check Real.log
|
||||
#check ComplexConjugate.conj
|
||||
#check Complex.exp
|
||||
|
||||
theorem SimpleCauchyFormula :
|
||||
∀
|
||||
{R : ℝ} -- Radius of the ball
|
||||
{w : ℂ} -- Point in the interior of the ball
|
||||
{f : ℂ → ℂ}, -- Holomorphic function
|
||||
Differentiable ℂ f
|
||||
→ w ∈ Metric.ball 0 R
|
||||
→ (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by
|
||||
|
||||
intro R w f fHyp
|
||||
|
||||
apply DiffContOnCl.circleIntegral_sub_inv_smul
|
||||
|
||||
constructor
|
||||
· exact Differentiable.differentiableOn fHyp
|
||||
· suffices Continuous f from by
|
||||
exact Continuous.continuousOn this
|
||||
rw [continuous_iff_continuousAt]
|
||||
intro x
|
||||
exact DifferentiableAt.continuousAt (fHyp x)
|
||||
|
||||
|
||||
theorem JensenFormula₂ :
|
||||
∀
|
||||
{R : ℝ} -- Radius of the ball
|
||||
{f : ℂ → ℂ}, -- Holomorphic function
|
||||
Differentiable ℂ f
|
||||
→ (∀ z ∈ Metric.ball 0 R, f z ≠ 0)
|
||||
→ (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * Complex.log ‖f 0‖ := by
|
||||
|
||||
intro r f fHyp₁ fHyp₂
|
||||
|
||||
/- We treat the trivial case r = 0 separately. -/
|
||||
by_cases rHyp : r = 0
|
||||
rw [rHyp]
|
||||
simp
|
||||
left
|
||||
unfold ENNReal.ofReal
|
||||
simp
|
||||
rw [max_eq_left (mul_nonneg zero_le_two pi_nonneg)]
|
||||
simp
|
||||
/- From hereon, we assume that r ≠ 0. -/
|
||||
|
||||
/- Replace the integral over 0 … 2π by a circle integral -/
|
||||
suffices (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) = 2 * ↑π * Complex.log ↑‖f 0‖ from by
|
||||
have : ∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ↑‖f (circleMap 0 r θ)‖ = (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) := by
|
||||
have : (fun θ ↦ Complex.log ‖f (circleMap 0 r θ)‖) = (fun θ ↦ ((deriv (circleMap 0 r) θ)) • ((deriv (circleMap 0 r) θ)⁻¹ • Complex.log ↑‖f (circleMap 0 r θ)‖)) := by
|
||||
funext θ
|
||||
rw [← smul_assoc, smul_eq_mul, smul_eq_mul, mul_inv_cancel, one_mul]
|
||||
simp
|
||||
exact rHyp
|
||||
rw [this]
|
||||
simp
|
||||
let tmp := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r
|
||||
simp at tmp
|
||||
rw [← tmp]
|
||||
rw [this]
|
||||
|
||||
|
||||
|
||||
have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by
|
||||
intro z
|
||||
|
||||
by_cases argHyp : Complex.arg z = π
|
||||
|
||||
· rw [Complex.log, argHyp, Complex.log]
|
||||
let ZZ := Complex.arg_conj z
|
||||
rw [argHyp] at ZZ
|
||||
|
||||
simp at ZZ
|
||||
|
||||
have : conj z = z := by
|
||||
apply?
|
||||
sorry
|
||||
|
||||
let ZZ := Complex.log_conj z
|
||||
|
||||
nth_rewrite 1 [Complex.log]
|
||||
|
||||
simp
|
||||
|
||||
let φ := Complex.arg z
|
||||
let r := Complex.abs z
|
||||
have : z = r * Complex.exp (φ * Complex.I) := by
|
||||
exact (Complex.abs_mul_exp_arg_mul_I z).symm
|
||||
|
||||
have : Complex.log z = Complex.log r + r*Complex.I := by
|
||||
apply?
|
||||
sorry
|
||||
simp at XX
|
||||
|
||||
|
||||
sorry
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
sorry
|
|
@ -1,11 +1,10 @@
|
|||
{"version": "1.1.0",
|
||||
{"version": "1.0.0",
|
||||
"packagesDir": ".lake/packages",
|
||||
"packages":
|
||||
[{"url": "https://github.com/leanprover-community/batteries",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
|
||||
"rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
|
||||
"name": "batteries",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
|
@ -14,8 +13,7 @@
|
|||
{"url": "https://github.com/leanprover-community/quote4",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
|
||||
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
|
||||
"name": "Qq",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
@ -24,8 +22,7 @@
|
|||
{"url": "https://github.com/leanprover-community/aesop",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
|
||||
"rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
|
||||
"name": "aesop",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "master",
|
||||
|
@ -34,48 +31,34 @@
|
|||
{"url": "https://github.com/leanprover-community/ProofWidgets4",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
|
||||
"rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
|
||||
"name": "proofwidgets",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "v0.0.42",
|
||||
"inputRev": "v0.0.38",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover/lean4-cli",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
|
||||
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
|
||||
"name": "Cli",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover-community/import-graph",
|
||||
"configFile": "lakefile.lean"},
|
||||
{"url": "https://github.com/leanprover-community/import-graph.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "leanprover-community",
|
||||
"rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
|
||||
"rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
|
||||
"name": "importGraph",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
|
||||
"name": "LeanSearchClient",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": "main",
|
||||
"inherited": true,
|
||||
"configFile": "lakefile.toml"},
|
||||
{"url": "https://github.com/leanprover-community/mathlib4.git",
|
||||
"type": "git",
|
||||
"subDir": null,
|
||||
"scope": "",
|
||||
"rev": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1",
|
||||
"rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60",
|
||||
"name": "mathlib",
|
||||
"manifestFile": "lake-manifest.json",
|
||||
"inputRev": null,
|
||||
|
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.12.0-rc1
|
||||
leanprover/lean4:v4.9.0-rc3
|
||||
|
|
Loading…
Reference in New Issue