SourceRadiusFlux.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Mahler.continuousOn_sourceFluxForm_sphere line 12

theorem OAI.Mahler.sphereFlux_pos_eq_coordinateFlux line 19

Source documentation

Positive dilation of the coordinate integral uses the tangential degree 2k+1, with no change in the outward orientation.

theorem sphereFlux_pos_eq_coordinateFlux {k : ℕ} {r : ℝ} (hr : 0 < r)
    (B : ComplexEuclidean (k+1) → ComplexEuclidean (k+1) [⋀^Fin (2*k+1)]→L[ℝ] ℂ)
    (hB : ContinuousOn B (sphere 0 r)) :
    MahlerStokes.sphereFlux r (fluxPullback B) =
      r^(2*k+1) * sphereFlux k (fun x => (B (r • x)).toAlternatingMap) := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.MahlerStokes.sphereFlux, OAI.Mahler.fluxPullback, OAI.Mahler.sphereFlux

theorem OAI.Mahler.sourceCoordinateFlux_eq_radiusSphereFlux line 37
Source documentation
The coordinate Stokes flux equals the real part of the radius-sphere area integral. C3 is required only at the radius sphere.
```
theorem sourceCoordinateFlux_eq_radiusSphereFlux {k : ℕ}
    {u : ComplexEuclidean (k+1) → ℂ} {r : ℝ} (hr : 0 < r)
    (hu : ∀ z ∈ sphere (0 : ComplexEuclidean (k+1)) r, ContDiffAt ℝ 3 u z) :
    MahlerStokes.sphereFlux r (sourceCoordinateForm (sourceCoordinates k) u k) =
      (radiusSphereFlux k u r).re := by
…
```
Mentions: OAI.Mahler.ComplexEuclidean, OAI.MahlerStokes.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.radiusSphereFlux

theorem OAI.Mahler.MassHypotheses.sourceCoordinateFlux_eq_radiusSphereFlux line 81

Source documentation

The mass hypotheses supply every regularity premise. Only the positive radius and inclusion of its sphere in the source domain remain.

theorem MassHypotheses.sourceCoordinateFlux_eq_radiusSphereFlux {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)
    {r : ℝ} (hr : 0 < r) (hSU : sphere (0 : ComplexEuclidean (k+1)) r ⊆ U) :
    MahlerStokes.sphereFlux r (sourceCoordinateForm (sourceCoordinates k) (logTau f) k) =
      (radiusSphereFlux k (logTau f) r).re := by
…

Mentions: OAI.Mahler.ComplexEuclidean, OAI.Mahler.MassHypotheses, OAI.MahlerStokes.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.logTau, OAI.Mahler.radiusSphereFlux

theorem OAI.Mahler.MassHypotheses.sourceCoordinateFlux_limit line 96

Source documentation

The coordinate small-sphere limit, with no flux-bridge premise.

theorem MassHypotheses.sourceCoordinateFlux_limit {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) :
    Tendsto (fun r => MahlerStokes.sphereFlux r
      (sourceCoordinateForm (sourceCoordinates k) (logTau f) k))
      (𝓝[>] 0) (𝓝 (homogeneousSphereFlux k N G)) := by
…