HomogeneousPrimitiveRegularity.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.contDiffAt_form_eval line 12

Source documentation

Evaluation at a fixed tuple preserves finite-order regularity.

lemma contDiffAt_form_eval {E X ι : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup X] [NormedSpace ℝ X] [Fintype ι]
    {a : X → E [⋀^ι]→L[ℝ] ℂ} {x : X} (q : ℕ)
    (ha : ContDiffAt ℝ q a x) (v : ι → E) :
    ContDiffAt ℝ q (fun y => a y v) x := by
…

lemma OAI.Mahler.contDiffAt_extDeriv_order line 24
def OAI.Mahler.sourcePrimitiveSlots line 32
Source documentation
The order alpha, beta, followed by k ordered d-alpha factors.
```
def sourcePrimitiveSlots (k : ℕ) :
    (Fin 1 ⊕ (Fin 1 ⊕ WedgePowerSlots k)) ≃ Fin (2*(k+1)) :=
…
```
Mentions: OAI.Mahler.WedgePowerSlots
def OAI.Mahler.sourcePrimitiveFin line 36
def OAI.Mahler.sourceHomogeneousPrimitive line 47
Source documentation
The literal homogeneous primitive, continuously bundled by exact finite basis expansion. No exterior differentiation identity is assumed here.
```
def sourceHomogeneousPrimitive {k N m : ℕ}
    (G : Fin N → MvPolynomial (Fin (k+2)) ℂ) (t : ℝ)
    (x : ComplexEuclidean (k+2)) :
    ComplexEuclidean (k+2) [⋀^Fin (2*(k+1))]→L[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean
theorem OAI.Mahler.sourceHomogeneousPrimitive_eq line 55
theorem OAI.Mahler.MassHypotheses.sourceHomogeneousPrimitive_contDiffAt line 63
theorem OAI.Mahler.MassHypotheses.sourceHomogeneousPrimitive_C2 line 83