SourceRegularLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Mahler.source_eventually_ball_subset_sublevel line 14
Source documentation
Small balls really lie in the source sublevel eventually; this is derived from the isolated zero and local continuity, not assumed.
```
theorem source_eventually_ball_subset_sublevel (h : MassHypotheses (k+1) N m U f G)
    {R : ℝ} (hR : 0 < R) :
    ∀ᶠ r in 𝓝[>] (0 : ℝ), coordClosedBall ((2*k+1)+1) r ⊆
      regularSublevel ((sourceCoordinates k) ⁻¹' U) (fun x => tau f (sourceCoordinates k x)) R := by
…
```
Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.sourceCoordinates, OAI.Mahler.tau

theorem OAI.Mahler.source_regular_mass_lower_of_flux_limit line 35

Source documentation

A limit L of outward Stokes sphere flux gives a regular-level mass bound R^n L. No Stokes identity, positivity, or ball-inclusion premise remains.

theorem source_regular_mass_lower_of_flux_limit (h : MassHypotheses (k+1) N m U f G)
    {R L : ℝ} (hR : 0 < R) (hR1 : R < 1)
    (hreg : ∀ z ∈ U, tau f z = R → fderiv ℝ (tau f) z ≠ 0)
    (hlimit : Tendsto
      (fun r => sphereFlux r (sourceCoordinateForm (sourceCoordinates k) (logTau f) k))
      (𝓝[>] (0 : ℝ)) (𝓝 L)) :
    R^(k+1) * L ≤ ∫ z in U ∩ {z | tau f z < R}, massDensity f z := by
…

Mentions: OAI.Mahler.MassHypotheses, OAI.Mahler.tau, OAI.Mahler.sphereFlux, OAI.Mahler.sourceCoordinateForm, OAI.Mahler.sourceCoordinates, OAI.Mahler.logTau, OAI.Mahler.massDensity