LogScalarJet.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SymmetricMahler.logD line 16
def OAI.SymmetricMahler.logD2 line 18
lemma OAI.SymmetricMahler.hasFDerivAt_logD line 21

lemma OAI.SymmetricMahler.fderiv_log_twice line 29

Source documentation

Actual nested real derivative, from the local derivative field and the inverse/product rule. Positivity is used locally, not assumed as a log jet.

lemma fderiv_log_twice {f : E → ℝ} {a : E → (E →L[ℝ] ℝ)}
    {b : E →L[ℝ] (E →L[ℝ] ℝ)} {x : E}
    (hf : ∀ᶠ y in 𝓝 x, HasFDerivAt f (a y) y)
    (ha : HasFDerivAt a b x) (hx : f x ≠ 0) :
    fderiv ℝ (fderiv ℝ (fun y => Real.log (f y))) x = logD2 (f x) (a x) b := by
…

Mentions: OAI.SymmetricMahler.logD2

theorem OAI.SymmetricMahler.uniform_log_jets line 44

Source documentation

Uniform convergence of the explicit logarithmic jets. The positive cutoff makes each algebraic operation globally continuous; it agrees with the actual formula on the limit and eventually on the entire compact set.

theorem uniform_log_jets [FiniteDimensional ℝ E]
    {I X : Type*} [TopologicalSpace X] {K : Set X} {l : Filter I}
    {u : I → X → ℝ} {a : I → X → (E →L[ℝ] ℝ)}
    {b : I → X → (E →L[ℝ] (E →L[ℝ] ℝ))}
    {t : X → ℝ} {A : X → (E →L[ℝ] ℝ)} {B : X → (E →L[ℝ] (E →L[ℝ] ℝ))}
    (hK : IsCompact K) (ht : ContinuousOn t K) (hA : ContinuousOn A K)
    (hB : ContinuousOn B K) (hp : ∀ x ∈ K, 0 < t x)
    (hu : TendstoUniformlyOn u t l K) (ha : TendstoUniformlyOn a A l K)
    (hb : TendstoUniformlyOn b B l K) :
    (∃ c : ℝ, 0 < c ∧ ∀ᶠ i in l, ∀ x ∈ K, c ≤ u i x) ∧
    TendstoUniformlyOn (fun i x => Real.log (u i x)) (fun x => Real.log (t x)) l K ∧
    TendstoUniformlyOn (fun i x => logD (u i x) (a i x))
…

Mentions: OAI.SymmetricMahler.logD