OAI/Analysis/Mahler/HomogeneousVariationCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.wedge_wedgePowerVariation_succ line 8
2. def OAI.Mahler.boundarySingleResidualFin line 27

   Source documentation

   The residual with one explicit d beta factor and no suppressed placements. The intermediate slot type keeps the original recursive order.

   noncomputable def boundarySingleResidualFin {k : ℕ}
       (a b : ComplexEuclidean (k+2) → ComplexEuclidean (k+2) →L[ℝ] ℂ)
       (x : ComplexEuclidean (k+2)) :
       ComplexEuclidean (k+2) [⋀^Fin (2*(k+1)+1)]→ₗ[ℝ] ℂ :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean

3. theorem OAI.Mahler.boundaryResidualFin_succ line 38

   Source documentation

   All residual placements combine with the positive multiplicity k+1. The residual is retained; its integral is not assumed to vanish.

   theorem boundaryResidualFin_succ {k : ℕ}
       (a b : ComplexEuclidean (k+2) → ComplexEuclidean (k+2) →L[ℝ] ℂ)
       (x : ComplexEuclidean (k+2)) :
       boundaryResidualFin (k := k+1) a b x =
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.boundaryResidualFin