HomogeneousEndpoint.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.sourcePrimitiveSlots_eq_primitiveFinEquiv line 14
Source documentation
The two independent continuous primitive constructions use the same ordered slots: alpha, beta, followed by the interleaved d-alpha factors.
```
lemma sourcePrimitiveSlots_eq_primitiveFinEquiv (k : ℕ) :
    sourcePrimitiveSlots k = primitiveFinEquiv k := by
…
```
Mentions: OAI.Mahler.sourcePrimitiveSlots, OAI.Mahler.primitiveFinEquiv
lemma OAI.Mahler.sourceHomogeneousPrimitive_eq_homogeneousPrimitive line 24
Source documentation
Equality of the actual continuous fields identifies their exterior derivatives; no additional integration or regularity premise is introduced.
```
lemma sourceHomogeneousPrimitive_eq_homogeneousPrimitive {k N m : ℕ}
    (G : Fin N → MvPolynomial (Fin (k+2)) ℂ) (t : ℝ) :
    sourceHomogeneousPrimitive (m := m) G t = homogeneousPrimitive (m := m) G t := by
…
```
Mentions: OAI.Mahler.sourceHomogeneousPrimitive, OAI.Mahler.homogeneousPrimitive

theorem OAI.Mahler.MassHypotheses.homogeneous_flux_endpoints line 35

Source documentation

The homogeneous value and radius-sphere limit in all complex dimensions at least two, from the mass hypotheses alone.

theorem MassHypotheses.homogeneous_flux_endpoints {k N m : ℕ}
    {U : Set (ComplexEuclidean (k+2))} {f : Fin N → ComplexEuclidean (k+2) → ℂ}
    {G : Fin N → MvPolynomial (Fin (k+2)) ℂ} (h : MassHypotheses (k+2) N m U f G) :
    homogeneousSphereFlux (k+1) N G = (Real.pi*(m:ℝ))^(k+2) ∧
    Tendsto (fun r => (radiusSphereFlux (k+1) (logTau f) r).re)
      (𝓝[>] (0:ℝ)) (𝓝 ((Real.pi*(m:ℝ))^(k+2))) := by
…

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

theorem OAI.Mahler.MassHypotheses.homogeneousSphereFlux_value line 49
Source documentation
The numerical homogeneous flux in every positive complex dimension. Dimension one is handled by the already proved circle calculation.
```
theorem MassHypotheses.homogeneousSphereFlux_value {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) := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.Mahler.homogeneousSphereFlux