OAI/Analysis/Mahler/RealLogBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.complexifyDerivative line 12
2. def OAI.Mahler.complexifySecondDerivative line 14
3. lemma OAI.Mahler.fderiv_ofReal_eq line 18
4. lemma OAI.Mahler.fderiv_twice_ofReal_eq line 23
5. theorem OAI.Mahler.uniform_log_jets_ofReal line 36

   Source documentation

   Scalar extension from real log jets to complex-valued real differential forms.

   theorem uniform_log_jets_ofReal [FiniteDimensional ℝ E]
       {I : Type*} {l : Filter I} {u : I → E → ℝ} {v : E → ℝ} {K : Set E}
       (hK : IsCompact K) (hv : ∀ x ∈ K, ContDiffAt ℝ 2 v x)
       (hu : ∀ᶠ i in l, ∀ x ∈ K, ContDiffAt ℝ 2 (u i) x)
       (h1 : TendstoUniformlyOn (fun i => fderiv ℝ (u i)) (fderiv ℝ v) l K)
       (h2 : TendstoUniformlyOn (fun i => fderiv ℝ (fderiv ℝ (u i))) (fderiv ℝ (fderiv ℝ v)) l K) :
       TendstoUniformlyOn (fun i => fderiv ℝ (fun x => (u i x : ℂ)))
         (fderiv ℝ (fun x => (v x : ℂ))) l K ∧
       TendstoUniformlyOn (fun i => fderiv ℝ (fderiv ℝ (fun x => (u i x : ℂ))))
         (fderiv ℝ (fderiv ℝ (fun x => (v x : ℂ)))) l K := by
   …

6. lemma OAI.Mahler.sphereAnnulus_eq_logCompactAnnulus line 68
7. theorem OAI.Mahler.MassHypotheses.small_sphere_flux_limit line 73