HomogeneousFluxFTC.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.MassHypotheses.homogeneousResidualFlux_continuous line 12

Source documentation

The residual flux is continuous on the entire parameter line.

theorem MassHypotheses.homogeneousResidualFlux_continuous {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) :
    Continuous (fun t => sphereFlux k (boundaryResidualFin
      (alphaPath (polynomialMap G) (coordinateMap (k+1)) m t)
      (betaLinear (polynomialMap G) (coordinateMap (k+1)) m))) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.sphereFlux, OAI.Mahler.boundaryResidualFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.betaLinear

theorem OAI.Mahler.MassHypotheses.homogeneousPathFlux_sub_eq_integral line 24
Source documentation
A finite, integrated variation formula for the literal homogeneous path. This supplies endpoint control as well as the pointwise derivative. The exact residual integral is not replaced by zero.
```
theorem MassHypotheses.homogeneousPathFlux_sub_eq_integral {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)
    (a b : ℝ) :
    homogeneousPathFlux k N m G b - homogeneousPathFlux k N m G a =
      ∫ t in a..b, sphereFlux k (boundaryResidualFin
        (alphaPath (polynomialMap G) (coordinateMap (k+1)) m t)
        (betaLinear (polynomialMap G) (coordinateMap (k+1)) m)) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousPathFlux, OAI.Mahler.sphereFlux, OAI.Mahler.boundaryResidualFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.betaLinear

theorem OAI.Mahler.MassHypotheses.homogeneousSphereFlux_sub_reference line 38

Source documentation

Actual endpoint discrepancy from the reference value, with only the remaining integrated residual on the right-hand side.

theorem MassHypotheses.homogeneousSphereFlux_sub_reference {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) :
    homogeneousSphereFlux k N G - (Real.pi * (m : ℝ))^(k+1) =
      ∫ t in (0 : ℝ)..1, sphereFlux k (boundaryResidualFin
        (alphaPath (polynomialMap G) (coordinateMap (k+1)) m t)
        (betaLinear (polynomialMap G) (coordinateMap (k+1)) m)) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousSphereFlux, OAI.Mahler.sphereFlux, OAI.Mahler.boundaryResidualFin, OAI.Mahler.alphaPath, OAI.Mahler.polynomialMap, OAI.Mahler.coordinateMap, OAI.Mahler.betaLinear