OAI/Analysis/Mahler/HomogeneousTransgression.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.homogeneousPrimitive line 10

   Source documentation

   The transgression primitive in every complex dimension k+2.

   noncomputable def homogeneousPrimitive {k N m : ℕ}
       (G : Fin N → MvPolynomial (Fin (k+2)) ℂ) (t : ℝ) :=
   …

2. lemma OAI.Mahler.homogeneousPrimitive_is_wedge line 16
3. theorem OAI.Mahler.MassHypotheses.homogeneousPrimitive_extDeriv line 27

   Source documentation

   The full ambient identity; the horizontal term has not been discarded.

   theorem MassHypotheses.homogeneousPrimitive_extDeriv {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
       {x : ComplexEuclidean (k+2)} (hx : x ≠ 0) (t : ℝ) :
       (extDeriv (homogeneousPrimitive (m := m) G t) x).toAlternatingMap =
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousPrimitive

4. theorem OAI.Mahler.MassHypotheses.homogeneousPrimitive_contDiffAt line 55

   Source documentation

   Every required smoothness order follows from MassHypotheses.

   theorem MassHypotheses.homogeneousPrimitive_contDiffAt {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
       {x : ComplexEuclidean (k+2)} (hx : x ≠ 0) (t : ℝ) (q : ℕ) :
       ContDiffAt ℝ q (homogeneousPrimitive (m := m) G t) x :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousPrimitive

5. theorem OAI.Mahler.MassHypotheses.sphere_residual_transgression line 65

   Source documentation

   Exact negative-sign residual transgression on sphere tangents, with the actual multiplicity n-1, in all complex dimensions n=k+2.

   theorem MassHypotheses.sphere_residual_transgression {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
       {x : ComplexEuclidean (k+2)} (hx : x ≠ 0) (t : ℝ)
       (v : Fin (2*(k+1)+1) → ComplexEuclidean (k+2))
       (hv : ∀ i, inner ℝ x (v i) = 0) :
       boundaryResidualFin (k := k+1)
   …

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

6. theorem OAI.Mahler.MassHypotheses.sphere_density_transgression line 99
7. theorem OAI.Mahler.MassHypotheses.sphere_boundaryForm_transgression line 121

   Source documentation

   The actual boundary-form derivative on every tangent tuple.

   theorem MassHypotheses.sphere_boundaryForm_transgression {k N m : ℕ}
       {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
       {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G)
       {x : ComplexEuclidean (k+2)} (hx : x ≠ 0) (t : ℝ)
       (v : Fin (2*(k+1)+1) → ComplexEuclidean (k+2))
       (hv : ∀ i, inner ℝ x (v i) = 0) :
       HasDerivAt
         (fun s => boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap (k+2)) m s) x v)
         (-((k+1 : ℕ) : ℂ) * extDeriv (homogeneousPrimitive (m := m) G t) x v) t := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.boundaryFormFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.homogeneousPrimitive