OAI/Analysis/Mahler/SourceRegularFlux.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Mahler.source_regular_flux_le_mass line 17

   Source documentation

   The punctured Stokes inequality for the coordinate forms, Hessian mass density, outward inner sphere, and ordinary complex volume. Only the geometric inclusion of the small closed ball is a premise.

   theorem source_regular_flux_le_mass (h : MassHypotheses (k+1) N m U f G)
       {R r : ℝ} (hR : 0 < R) (hR1 : R < 1)
       (hreg : ∀ z ∈ U, tau f z = R → fderiv ℝ (tau f) z ≠ 0)
       (hr : 0 < r)
       (hB : coordClosedBall ((2*k+1)+1) r ⊆
         regularSublevel ((sourceCoordinates k) ⁻¹' U) (fun x => tau f (sourceCoordinates k x)) R) :
       sphereFlux r (sourceCoordinateForm (sourceCoordinates k) (logTau f) k) ≤
         (R⁻¹)^(k+1) * (∫ z in U ∩ {z | tau f z < R}, massDensity f z) := by
   …

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