HomogeneousSmoothForms.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.contDiffAt_logTau_order line 13

Source documentation

The required local smoothness follows from the literal holomorphic data, for every finite order, wherever tau is positive.

lemma contDiffAt_logTau_order [FiniteDimensional ℂ E]
    {ι : Type*} [Fintype ι] {f : ι → E → ℂ} {U : Set E} {x : E}
    (q : ℕ) (hU : IsOpen U) (hx : x ∈ U)
    (hf : ∀ j, DifferentiableOn ℂ (f j) U) (ht : 0 < tau f x) :
    ContDiffAt ℝ q (logTau f) x := by
…

Mentions: OAI.Mahler.tau, OAI.Mahler.logTau

lemma OAI.Mahler.contDiffAt_dcLinear_order line 29
lemma OAI.Mahler.contDiffAt_oneForm_order line 35
theorem OAI.Mahler.MassHypotheses.alpha_beta_contDiffAt line 39

theorem OAI.Mahler.MassHypotheses.alphaPath_extDeriv_extDeriv line 58

Source documentation

The d squared term vanishes along the homogeneous path; no closedness or higher smoothness premise is added.

theorem MassHypotheses.alphaPath_extDeriv_extDeriv {n N m : ℕ}
    {U : Set (ComplexEuclidean n)} {f : Fin N → ComplexEuclidean n → ℂ}
    {G : Fin N → MvPolynomial (Fin n) ℂ} (h : MassHypotheses n N m U f G)
    {z : ComplexEuclidean n} (hz : z ≠ 0) (t : ℝ) :
    extDeriv (extDeriv (oneForm (alphaPath (polynomialMap G) (coordinateMap n) m t))) z = 0 := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.oneForm, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap