OAI/Analysis/Mahler/LogNormSquare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SymmetricMahler.actualComplexTwoJet line 15
2. lemma OAI.SymmetricMahler.C2_log_normSq_derivatives line 19
3. lemma OAI.SymmetricMahler.continuousOn_actualComplexTwoJet line 42
4. lemma OAI.SymmetricMahler.uniform_actualComplexTwoJet line 52
5. theorem OAI.SymmetricMahler.uniform_C2_log_sumNormSq line 69

   Source documentation

   The analytic composition passage in the fixed-annulus argument. Every convergence hypothesis concerns the original complex functions and their actual complex derivatives. Every derivative in the conclusion is an actual real Fréchet derivative of the logarithm of the finite norm sum.

   theorem uniform_C2_log_sumNormSq [FiniteDimensional ℂ E] [FiniteDimensional ℝ E]
       {I : Type*} {l : Filter I} {K U : Set E} {f : I → J → E → ℂ} {g : J → E → ℂ}
       (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U)
       (hg : ∀ j, ContDiffOn ℂ 2 (g j) U)
       (hf : ∀ᶠ i in l, ∀ j, ContDiffOn ℂ 2 (f i j) U)
       (hp : ∀ x ∈ K, 0 < ∑ j, Complex.normSq (g j x))
       (h0 : ∀ j, TendstoUniformlyOn (fun i => f i j) (g j) l K)
       (h1 : ∀ j, TendstoUniformlyOn (fun i => fderiv ℂ (f i j)) (fderiv ℂ (g j)) l K)
       (h2 : ∀ j, TendstoUniformlyOn (fun i => fderiv ℂ (fderiv ℂ (f i j)))
         (fderiv ℂ (fderiv ℂ (g j))) l K) :
       (∃ c : ℝ, 0 < c ∧ ∀ᶠ i in l, ∀ x ∈ K, c ≤ ∑ j, Complex.normSq (f i j x)) ∧
       TendstoUniformlyOn (fun i x => Real.log (∑ j, Complex.normSq (f i j x)))
   …