BoundaryDensity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SmoothObstruction.HalfspaceCollar.closedBall_interior line 13
Source documentation
Positive normal coordinate margin keeps the entire nonlinear tube in the original half-space. No extension across the boundary is used.
```
theorem closedBall_interior {d : ℕ} [NeZero d] (x : EuclideanSpace ℝ (Fin d))
    {δ : ℝ} (hx : δ<x 0) : closedBall x δ⊆interior (Set.range (𝓡∂ d)) := by
…
```
theorem OAI.SmoothObstruction.HalfspaceCollar.slab_volume_le line 27
Source documentation
The elementary quantitative codimension-one collar bound. Merely knowing that the boundary is null would not imply the simultaneous [-n,n] retained-mass estimate required in smooth switching.
```
theorem slab_volume_le {d : ℕ} (j : Fin d) (R ε : ℝ) :
    volume {x : EuclideanSpace ℝ (Fin d) | ‖x‖≤R ∧ 0≤x j ∧ x j≤ε}≤
      ENNReal.ofReal ε*(ENNReal.ofReal (2*R))^(d-1) := by
…
```

theorem OAI.SmoothObstruction.HalfspaceCollar.supported_density_slab line 68

Source documentation

A bounded ORIGINAL chart density supported in a bounded patch retains the linear collar bound; the density is neither renormalized nor replaced by a uniform conditional law.

theorem supported_density_slab {d : ℕ} (j : Fin d) (R ε : ℝ)
    (f : EuclideanSpace ℝ (Fin d) → ℝ≥0∞) (A : ℝ≥0∞)
    (hf : ∀ x,f x≤A) (hzero : ∀ x,R<‖x‖ → f x=0) :
    (volume.withDensity f) {x | 0≤x j ∧ x j≤ε}≤
      A*(ENNReal.ofReal ε*(ENNReal.ofReal (2*R))^(d-1)) := by
…

theorem OAI.SmoothObstruction.ChartDensity.compact_chart_slab line 110

Source documentation

Quantitative collar estimate in an authentic compact coordinate patch. The measure is the original smooth measure restricted to that patch.

theorem compact_chart_slab (hclosed : IsClosed (range I)) (μ : Measure M)
    (hμ : SmoothPositiveDensity I μ) (a : M) (K : Set M) (hK : IsCompact K)
    (hKU : K⊆(extChartAt I a).source) (j : Fin d) :
    ∃ R A : ℝ,0<R ∧ 0<A ∧ ∀ ε : ℝ,
      μ {x | x∈K ∧ 0≤coordinates I a x j ∧ coordinates I a x j≤ε}≤
        ENNReal.ofReal A*(ENNReal.ofReal ε*(ENNReal.ofReal (2*R))^(d-1)) := by
…

Mentions: OAI.SmoothObstruction.SmoothPositiveDensity, OAI.SmoothObstruction.ChartDensity.coordinates

theorem OAI.SmoothObstruction.ChartDensity.global_halfspace_collar line 184

Source documentation

A GLOBAL quantitative boundary exclusion from the given original positive smooth density and authentic finite compact atlas. The same set works for every selected chart containing the point; its mass is O(δ), not merely o(1), so all 2n+1 tests can be charged to invariant volume.

theorem global_halfspace_collar (μ : Measure M) [IsFiniteMeasure μ]
    (hμ : SmoothPositiveDensity (𝓡∂ d) μ) (a : ι → M) (K : ι → Set M)
    (hK : ∀ i,IsCompact (K i)) (hKU : ∀ i,K i⊆(chartAt (EuclideanHalfSpace d) (a i)).source) :
    ∃ C : ℝ,0<C ∧ ∀ δ : ℝ,0≤δ →
      ∃ W : Set M,MeasurableSet W ∧ μ.real W≤C*δ ∧
        ∀ i x,x∈K i → x∉W →
          closedBall ((extChartAt (𝓡∂ d) (a i)) x) δ⊆interior (range (𝓡∂ d)) := by
…

Mentions: OAI.SmoothObstruction.SmoothPositiveDensity