OAI/Analysis/Mahler/FluxVariation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Mahler.oneForm_add line 13
2. lemma OAI.Mahler.oneForm_smul line 19
3. lemma OAI.Mahler.extDeriv_oneForm_affine line 24
4. theorem OAI.Mahler.hasDerivAt_boundaryForm line 33

   Source documentation

   Actual parameter derivative of the boundary form, at each vector tuple. The spatial derivatives are exterior derivatives.

   theorem hasDerivAt_boundaryForm {a b : E → E →L[ℝ] ℂ} {x : E}
       (ha : DifferentiableAt ℝ a x) (hb : DifferentiableAt ℝ b x)
       (S : Submodule ℝ E) (t : ℝ) (k : ℕ) (v : Fin 1 ⊕ WedgePowerSlots k → S) :
       HasDerivAt
         (fun s => wedge
           ((oneForm (a+s • b) x).toAlternatingMap.compLinearMap S.subtype)
           (wedgePower ((extDeriv (oneForm (a+s • b)) x).toAlternatingMap.compLinearMap S.subtype) k) v)
         ((wedge ((oneForm b x).toAlternatingMap.compLinearMap S.subtype)
           (wedgePower ((extDeriv (oneForm (a+t • b)) x).toAlternatingMap.compLinearMap S.subtype) k) +
           wedge ((oneForm (a+t • b) x).toAlternatingMap.compLinearMap S.subtype)
             (wedgePowerVariation
               ((extDeriv (oneForm (a+t • b)) x).toAlternatingMap.compLinearMap S.subtype)
   …

   Mentions: OAI.Mahler.WedgePowerSlots, OAI.Mahler.wedge, OAI.Mahler.oneForm, OAI.Mahler.wedgePower, OAI.Mahler.wedgePowerVariation

5. theorem OAI.Mahler.MassHypotheses.sphere_boundaryForm_derivative line 66

   Source documentation

   The first variation term vanishes for the homogeneous path. The remaining term is displayed explicitly; this is not flux constancy.

   theorem MassHypotheses.sphere_boundaryForm_derivative {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 : ℝ)
       (v : Fin 1 ⊕ WedgePowerSlots (n-1) → sphereTangent z) :
       HasDerivAt
         (fun s => wedge
           (tangentForm z (oneForm (alphaPath (polynomialMap G) (coordinateMap n) m s) z).toAlternatingMap)
           (wedgePower (tangentForm z
             (extDeriv (oneForm (alphaPath (polynomialMap G) (coordinateMap n) m s)) z).toAlternatingMap) (n-1)) v)
         (wedge
           (tangentForm z (oneForm (alphaPath (polynomialMap G) (coordinateMap n) m t) z).toAlternatingMap)
   …

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