OAI/Analysis/Mahler/SphereForms.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.coordinateMap line 11
2. lemma OAI.Mahler.coordinateMap_differentiable line 13
3. lemma OAI.Mahler.coordinateMap_homogeneous line 16
4. lemma OAI.Mahler.coordinateMap_tau_pos line 21
5. def OAI.Mahler.sphereTangent line 31

   Source documentation

   The tangent hyperplane of a Euclidean sphere, with its usual real metric.

   noncomputable def sphereTangent {n : ℕ} (z : ComplexEuclidean n) : Submodule ℝ (ComplexEuclidean n) :=
   …

   Mentions: OAI.Mahler.ComplexEuclidean

6. lemma OAI.Mahler.circle_mem_sphereTangent line 34
7. def OAI.Mahler.circleTangent line 40
8. lemma OAI.Mahler.circleTangent_ne_zero line 43
9. lemma OAI.Mahler.sphereTangent_finrank line 49
10. lemma OAI.Mahler.horizontal_twoForm line 58
11. def OAI.Mahler.tangentForm line 71
12. lemma OAI.Mahler.Horizontal.tangentForm line 75
13. theorem OAI.Mahler.MassHypotheses.sphere_beta_wedge_power_zero line 84

    Source documentation

    The top-degree deformation term vanishes on every sphere tangent space under the polynomial hypotheses.

    theorem MassHypotheses.sphere_beta_wedge_power_zero {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 : ℝ) :
        wedge
          (tangentForm z (oneForm (betaLinear (polynomialMap G) (coordinateMap n) m) z).toAlternatingMap)
          (wedgePower (tangentForm z
            (extDeriv (oneForm (alphaPath (polynomialMap G) (coordinateMap n) m t)) z).toAlternatingMap)
            (n - 1)) = 0 := by
    …

    Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.wedge, OAI.Mahler.tangentForm, OAI.Mahler.oneForm, OAI.Mahler.betaLinear, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.wedgePower, OAI.Mahler.alphaPath