DensityBounds.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SmoothObstruction.JacobianDomination.map_density_restrict_le line 24

Source documentation

Change of variables on the retained set itself. A density lower bound on the actual Jacobian gives domination without normalizing the retained measure. Global injectivity is essential here.

theorem map_density_restrict_le (μ : Measure E) [Measure.IsAddHaarMeasure μ]
    (d : E → ℝ≥0∞) (s : Set E) (hs : MeasurableSet s)
    (f : E → E) (hf : Measurable f) (J : E → E →L[ℝ] E)
    (hJ : ∀ x∈s,HasFDerivWithinAt f (J x) s x) (hinj : InjOn f s)
    (C : ℝ≥0∞) (hC : C≠∞)
    (hlower : ∀ x∈s,d x ≤ C*(ENNReal.ofReal |(J x).det| *d (f x))) :
    ((μ.withDensity d).restrict s).map f ≤ C • μ.withDensity d := by
…

theorem OAI.SmoothObstruction.JacobianDomination.local_branches_domination line 64

Source documentation

Agreement with genuine local derivative branches on relative retained neighborhoods gives a measurable total extension and the original retained-law domination. The within-set change-of-variables theorem avoids any assumption of measurable frame witnesses or measurable choices of local branches.

theorem local_branches_domination (μ : Measure E) [Measure.IsAddHaarMeasure μ]
    (d : E → ℝ≥0∞) (s : Set E) (hs : MeasurableSet s)
    (f : E → E) (J : E → E →L[ℝ] E)
    (hlocal : ∀ x∈s,∃ g : E → E,HasFDerivAt g (J x) x ∧ g =ᶠ[𝓝[s] x] f)
    (hinj : InjOn f s) (C : ℝ≥0∞) (hC : C≠∞)
    (hlower : ∀ x∈s,d x≤C*(ENNReal.ofReal |(J x).det| *d (f x))) :
    ∃ F : E → E,Measurable F ∧ EqOn F f s ∧
      ((μ.withDensity d).restrict s).map F≤C • μ.withDensity d := by
…

def OAI.SmoothObstruction.ChartDomination.coordinateSet line 97
Source documentation
The image of a measurable carrier under a measurable coordinate map with measurable inverse. Unlike an arbitrary image, this is visibly measurable.
```
def coordinateSet (e : X → E) (r : E → X) (G : Set X) : Set E :=
…
```
lemma OAI.SmoothObstruction.ChartDomination.measurable_coordinateSet line 100
lemma OAI.SmoothObstruction.ChartDomination.coordinateSet_eq_image line 107
theorem OAI.SmoothObstruction.ChartDomination.map_restrict_coordinateSet line 119
Source documentation
Restricting an ORIGINAL measure before taking chart coordinates is exactly restriction to the coordinate image, not conditioning on it. The chart inverse is required only on the full original carrier Q.
```
theorem map_restrict_coordinateSet (μ : Measure X)
    (Q G : Set X) (hQ : μ Qᶜ = 0)
    (e : X → E) (r : E → X) (he : Measurable e) (hr : Measurable r)
    (hG : MeasurableSet G) (hleft : ∀ x ∈ Q, r (e x) = x) :
    (μ.restrict G).map e = (μ.map e).restrict (coordinateSet e r G) := by
…
```
Mentions: OAI.SmoothObstruction.ChartDomination.coordinateSet

theorem OAI.SmoothObstruction.ChartDomination.local_domination line 138

Source documentation

A local coordinate change transfers a genuine retained-set smooth branch estimate back to the original measure. This provides a measurable extension in the original space without an assumed globally measurable frame choice. No retained mass is normalized, and the original carrier may be only Borel.

theorem local_domination (μ : Measure X) (m : Measure E)
    [Measure.IsAddHaarMeasure m] (d : E → ℝ≥0∞)
    (Q G : Set X) (hQ : μ Qᶜ = 0) (hGQ : G ⊆ Q) (hG : MeasurableSet G)
    (e : X → E) (r : E → X) (he : Measurable e) (hr : Measurable r)
    (hleft : ∀ x∈Q,r (e x)=x) (hcoords : μ.map e=m.withDensity d)
    (f : X → X) (hfQ : MapsTo f G Q)
    (φ : E → E) (J : E → E →L[ℝ] E)
    (hcompat : ∀ x∈G,φ (e x)=e (f x))
    (hlocal : ∀ u∈coordinateSet e r G,
      ∃ g : E → E, HasFDerivAt g (J u) u ∧
        g =ᶠ[𝓝[coordinateSet e r G] u] φ)
    (hinj : InjOn φ (coordinateSet e r G)) (C : ℝ≥0∞) (hC : C≠∞)
…

Mentions: OAI.SmoothObstruction.ChartDomination.coordinateSet

lemma OAI.SmoothObstruction.ChartDensity.measurable_target line 188
def OAI.SmoothObstruction.ChartDensity.coordinates line 194
def OAI.SmoothObstruction.ChartDensity.inverse line 198
lemma OAI.SmoothObstruction.ChartDensity.measurable_coordinates line 202
lemma OAI.SmoothObstruction.ChartDensity.measurable_inverse line 207
lemma OAI.SmoothObstruction.ChartDensity.coordinates_eq line 214
lemma OAI.SmoothObstruction.ChartDensity.inverse_eq line 220
lemma OAI.SmoothObstruction.ChartDensity.inverse_coordinates line 226
theorem OAI.SmoothObstruction.ChartDensity.cell_density line 235
Source documentation
Coordinates for each ORIGINAL measurable subcell carry precisely its chart Lebesgue density, without conditioning on the cell or on a good set. All maps have measurable total extensions; their arbitrary values off the chart are irrelevant to the equality.
```
theorem cell_density (hclosed : IsClosed (range I)) (μ : Measure M)
    (hμ : SmoothPositiveDensity I μ) (a : M) :
    ∃ f : EuclideanSpace ℝ (Fin d) → ℝ,
      ContDiffOn ℝ ∞ f (extChartAt I a).target ∧
      (∀ u∈(extChartAt I a).target,0<f u) ∧
      ∀ Q : Set M,MeasurableSet Q → Q⊆(extChartAt I a).source →
        let W := ChartDomination.coordinateSet (coordinates I a) (inverse I a) Q
…
```
Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDomination.coordinateSet, OAI.SmoothObstruction.ChartDensity.coordinates, OAI.SmoothObstruction.ChartDensity.inverse