OAI/Analysis/Mahler/HomogeneousTwoTransgression.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.boundaryResidualFin_two line 12
2. def OAI.Mahler.homogeneousTwoPrimitive line 23

   Source documentation

   The transgression primitive in complex dimension two.

   noncomputable def homogeneousTwoPrimitive {N m : ℕ}
       (G : Fin N → MvPolynomial (Fin 2) ℂ) (t : ℝ) (x : ComplexEuclidean 2) :
       ComplexEuclidean 2 [⋀^Fin 2]→L[ℝ] ℂ :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean

3. theorem OAI.Mahler.MassHypotheses.sphere_residual_two_transgression line 31

   Source documentation

   Exact negative-sign transgression on actual sphere tangents in complex dimension two. The residual is an exterior derivative, not pointwise zero.

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

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

4. theorem OAI.Mahler.MassHypotheses.sphere_density_two_transgression line 65

   Source documentation

   The actual density derivative with its residual replaced by the negative exterior derivative.

   theorem MassHypotheses.sphere_density_two_transgression {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G)
       {x : ComplexEuclidean 2} (hx : ‖x‖ = 1) (t : ℝ) :
       HasDerivAt
         (fun s => orientedDensity (sphereFrame 1) (sphereVolume 1)
           (boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap 2) m s) x) x)
         (orientedDensity (sphereFrame 1) (sphereVolume 1)
           (- (extDeriv (homogeneousTwoPrimitive (m := m) G t) x).toAlternatingMap) x) t := by
   …

   Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.orientedDensity, OAI.Mahler.sphereFrame, OAI.Mahler.sphereVolume, OAI.Mahler.boundaryFormFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.homogeneousTwoPrimitive

5. theorem OAI.Mahler.MassHypotheses.homogeneousTwoPrimitive_contDiffAt line 86

   Source documentation

   The primitive has every finite order of local regularity off the origin, and in particular is C1 at the entire unit sphere.

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

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

6. theorem OAI.Mahler.MassHypotheses.sphere_boundaryForm_two_transgression line 96

   Source documentation

   The actual boundary form derivative itself, with no residual placeholder, on arbitrary sphere tangent tuples in complex dimension two.

   theorem MassHypotheses.sphere_boundaryForm_two_transgression {N m : ℕ}
       {U : Set (ComplexEuclidean 2)} {f : Fin N → ComplexEuclidean 2 → ℂ}
       {G : Fin N → MvPolynomial (Fin 2) ℂ} (h : MassHypotheses 2 N m U f G)
       {x : ComplexEuclidean 2} (hx : x ≠ 0) (t : ℝ)
       (v : Fin 3 → ComplexEuclidean 2) (hv : ∀ i, inner ℝ x (v i) = 0) :
       HasDerivAt
         (fun s => boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap 2) m s) x v)
         (-(extDeriv (homogeneousTwoPrimitive (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.homogeneousTwoPrimitive