HomogeneousCircleIntegral.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.wedge_zero_right line 10
lemma OAI.Mahler.boundaryResidualFin_zero_dim line 16

theorem OAI.Mahler.MassHypotheses.circle_density_const line 23

Source documentation

In complex dimension one there is no residual term. This is actual pointwise constancy of the oriented density, not an integral assumption.

theorem MassHypotheses.circle_density_const {N m : ℕ}
    {U : Set (ComplexEuclidean 1)} {f : Fin N → ComplexEuclidean 1 → ℂ}
    {G : Fin N → MvPolynomial (Fin 1) ℂ} (h : MassHypotheses 1 N m U f G)
    {x : ComplexEuclidean 1} (hx : ‖x‖ = 1) (s t : ℝ) :
    orientedDensity (sphereFrame 0) (sphereVolume 0)
      (boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap 1) m s) x) x =
    orientedDensity (sphereFrame 0) (sphereVolume 0)
      (boundaryFormFin (alphaPath (polynomialMap G) (coordinateMap 1) m t) x) x := 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

theorem OAI.Mahler.MassHypotheses.circle_flux_const line 40
Source documentation
Actual homogeneous flux constancy in dimension one, proved without integration by parts because the residual degree is zero. The higher- dimensional residual is not eliminated by this theorem.
```
theorem MassHypotheses.circle_flux_const {N m : ℕ}
    {U : Set (ComplexEuclidean 1)} {f : Fin N → ComplexEuclidean 1 → ℂ}
    {G : Fin N → MvPolynomial (Fin 1) ℂ} (h : MassHypotheses 1 N m U f G)
    (s t : ℝ) : homogeneousPathFlux 0 N m G s = homogeneousPathFlux 0 N m G t := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousPathFlux

theorem OAI.Mahler.MassHypotheses.homogeneousCircle_flux line 51

Source documentation

Full homogeneous sphere normalization for complex dimension one.

theorem MassHypotheses.homogeneousCircle_flux {N m : ℕ}
    {U : Set (ComplexEuclidean 1)} {f : Fin N → ComplexEuclidean 1 → ℂ}
    {G : Fin N → MvPolynomial (Fin 1) ℂ} (h : MassHypotheses 1 N m U f G) :
    homogeneousSphereFlux 0 N G = Real.pi * (m : ℝ) := by
…

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