HomogeneousDensityVariation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.wedgePowerVariation_compLinearMap line 9
def OAI.Mahler.boundaryResidualFin line 28
Source documentation
The residual variation, retaining all terms and the actual exterior spatial derivatives. Its sphere integral has not been asserted to vanish.
```
noncomputable def boundaryResidualFin {k : ℕ}
    (a b : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) →L[ℝ] ℂ)
    (x : ComplexEuclidean (k+1)) :
    ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→ₗ[ℝ] ℂ :=
…
```
Mentions: OAI.Mahler.ComplexEuclidean

theorem OAI.Mahler.MassHypotheses.sphere_density_derivative line 38

Source documentation

Pointwise parameter derivative of the actual oriented sphere density. The horizontal term is eliminated; the residual is kept explicit.

theorem MassHypotheses.sphere_density_derivative {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+1))} {f : Fin N → ComplexEuclidean (k+1) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+1)) ℂ} (h : MassHypotheses (k+1) N m U f G)
    {x : ComplexEuclidean (k+1)} (hx : ‖x‖ = 1) (t : ℝ) :
    HasDerivAt
      (fun s => orientedDensity (sphereFrame k) (sphereVolume k)
        (boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap (k+1)) m s) x) x)
      (orientedDensity (sphereFrame k) (sphereVolume k)
        (boundaryResidualFin (alphaPath (polynomialMap G) (coordinateMap (k+1)) m t)
          (betaLinear (polynomialMap G) (coordinateMap (k+1)) m) x) 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.boundaryResidualFin, OAI.Mahler.betaLinear