BoundaryStrip.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.volume_convex_boundary_strip_le line 14
Source documentation
The right boundary strip of a compact real interval has length at most its translation distance, even when the interval is shorter than that distance.
```
theorem volume_convex_boundary_strip_le
    {I : Set ℝ} (hI : IsCompact I) (hc : Convex ℝ I)
    {h : ℝ} (hh : 0 ≤ h) :
    volume {t | t ∈ I ∧ t + h ∉ I} ≤ ENNReal.ofReal h := by
…
```

theorem OAI.Problem358.prod_measure_boundary_strip_le line 38

Source documentation

Fubini converts the one-dimensional strip estimate into a product estimate. The hypotheses describe exactly the interval fibers needed by coordinate slicing.

theorem prod_measure_boundary_strip_le
    {X : Type*} [MeasurableSpace X] (μ : Measure X)
    {K : Set (X × ℝ)} (hK : MeasurableSet K)
    (hproj : MeasurableSet (Prod.fst '' K))
    (hcompact : ∀ x, IsCompact {t : ℝ | (x, t) ∈ K})
    (hconvex : ∀ x, Convex ℝ {t : ℝ | (x, t) ∈ K})
    {h : ℝ} (hh : 0 ≤ h) :
    (μ.prod volume) {p | p ∈ K ∧ (p.1, p.2 + h) ∉ K} ≤
      ENNReal.ofReal h * μ (Prod.fst '' K) := by
…

theorem OAI.Problem358.isCompact_vertical_fiber line 69

Source documentation

A vertical fiber of a compact set is compact.

theorem isCompact_vertical_fiber
    {X : Type*} [TopologicalSpace X] [T2Space X]
    {K : Set (X × ℝ)} (hK : IsCompact K) (x : X) :
    IsCompact {t : ℝ | (x, t) ∈ K} := by
…

theorem OAI.Problem358.compact_convex_prod_boundary_strip_le line 89

Source documentation

The vertical boundary strip of a compact convex body has product measure at most its width times the measure of the transverse projection.

theorem compact_convex_prod_boundary_strip_le
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    (μ : Measure X) {K : Set (X × ℝ)}
    (hK : IsCompact K) (hc : Convex ℝ K) {h : ℝ} (hh : 0 ≤ h) :
    (μ.prod volume) {p | p ∈ K ∧ (p.1, p.2 + h) ∉ K} ≤
      ENNReal.ofReal h * μ (Prod.fst '' K) := by
…

theorem OAI.Problem358.norm_integral_compact_convex_boundary_strip_le line 106

Source documentation

Any uniformly bounded integrand has an O(h) integral on the excluded strip.

theorem norm_integral_compact_convex_boundary_strip_le
    {X G : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    (μ : Measure X) {K : Set (X × ℝ)}
    (hK : IsCompact K) (hc : Convex ℝ K)
    (hproj : μ (Prod.fst '' K) ≠ ∞)
    {h C : ℝ} (hh : 0 ≤ h) (hC : 0 ≤ C)
    {f : X × ℝ → G} (hf : ∀ p ∈ K, ‖f p‖ ≤ C) :
    ‖∫ p in {p | p ∈ K ∧ (p.1, p.2 + h) ∉ K}, f p ∂(μ.prod volume)‖ ≤
      C * h * μ.real (Prod.fst '' K) := by
…

theorem OAI.Problem358.boundary_strip_le_of_coordinate_split line 135

Source documentation

The strip estimate transports through any measure-preserving linear coordinate split. This separates geometric slicing from the choice of Euclidean coordinates.

theorem boundary_strip_le_of_coordinate_split
    {V X : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    [MeasurableSpace V] [BorelSpace V]
    [NormedAddCommGroup X] [NormedSpace ℝ X]
    [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    (e : V ≃L[ℝ] (X × ℝ)) (η : Measure V) (μ : Measure X)
    (hpres : MeasurePreserving e η (μ.prod volume))
    {v : V} (hv : e v = (0, 1))
    {K : Set V} (hK : IsCompact K) (hc : Convex ℝ K)
    {h : ℝ} (hh : 0 ≤ h) :
    η {x | x ∈ K ∧ x + h • v ∉ K} ≤
      ENNReal.ofReal h * μ (Prod.fst '' (e '' K)) := by
…

theorem OAI.Problem358.convex_contraction_add_mem line 179

Source documentation

Contracting toward a point gives a translated core in a convex set.

theorem convex_contraction_add_mem {K : Set V} (hK : Convex ℝ K)
    {p e x : V} (hx : x ∈ K) (hpe : p + e ∈ K)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    (1 - t) • x + t • p + t • e ∈ K := by
…

theorem OAI.Problem358.convex_contraction_subset_shift_core line 187

Source documentation

The contracted image is in the forward translation core.

theorem convex_contraction_subset_shift_core {K : Set V} (hK : Convex ℝ K)
    {p e : V} (hp : p ∈ K) (hpe : p + e ∈ K)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    (fun x => (1 - t) • x + t • p) '' K ⊆
      {x | x ∈ K ∧ x + t • e ∈ K} := by
…

theorem OAI.Problem358.measureReal_contraction_image line 202

Source documentation

The Haar measure of an affine contraction, in real-valued form.

theorem measureReal_contraction_image (K : Set V) (p : V) {t : ℝ}
    (ht1 : t ≤ 1) :
    μ.real ((fun x => (1 - t) • x + t • p) '' K) =
      (1 - t) ^ Module.finrank ℝ V * μ.real K := by
…

theorem OAI.Problem358.measureReal_convex_shift_strip_le line 220

Source documentation

A geometric boundary strip is controlled by the volume lost under contraction.

theorem measureReal_convex_shift_strip_le {K : Set V} (hKc : IsCompact K)
    (hK : Convex ℝ K) {p e : V} (hp : p ∈ K) (hpe : p + e ∈ K)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    μ.real {x | x ∈ K ∧ x + t • e ∉ K} ≤
      (1 - (1 - t) ^ Module.finrank ℝ V) * μ.real K := by
…

theorem OAI.Problem358.measureReal_convex_shift_strip_le_linear line 243

Source documentation

Bernoulli gives a dimension-linear bound for the boundary strip.

theorem measureReal_convex_shift_strip_le_linear {K : Set V} (hKc : IsCompact K)
    (hK : Convex ℝ K) {p e : V} (hp : p ∈ K) (hpe : p + e ∈ K)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) :
    μ.real {x | x ∈ K ∧ x + t • e ∉ K} ≤
      Module.finrank ℝ V * t * μ.real K := by
…

theorem OAI.Problem358.measureReal_convex_shift_strip_le_of_closedBall line 257

Source documentation

Interior-ball specialization of the boundary estimate for small translations.

theorem measureReal_convex_shift_strip_le_of_closedBall {K : Set V}
    (hKc : IsCompact K) (hK : Convex ℝ K) {p : V} {r : ℝ} (hr : 0 < r)
    (hball : Metric.closedBall p r ⊆ K) {v : V} (hv : ‖v‖ ≤ 1)
    {h : ℝ} (hh0 : 0 ≤ h) (hhr : h ≤ r) :
    μ.real {x | x ∈ K ∧ x + h • v ∉ K} ≤
      Module.finrank ℝ V * (h / r) * μ.real K := by
…

theorem OAI.Problem358.measureReal_convex_shift_strip_le_all line 277

Source documentation

A single linear constant controls every translation length, not only small ones.

theorem measureReal_convex_shift_strip_le_all {K : Set V}
    (hKc : IsCompact K) (hK : Convex ℝ K) {p : V} {r : ℝ} (hr : 0 < r)
    (hball : Metric.closedBall p r ⊆ K) {v : V} (hv : ‖v‖ ≤ 1)
    {h : ℝ} (hh : 0 ≤ h) :
    μ.real {x | x ∈ K ∧ x + h • v ∉ K} ≤
      (max (Module.finrank ℝ V : ℝ) 1 * μ.real K / r) * h := by
…

theorem OAI.Problem358.exists_convex_boundary_strip_constant line 306

Source documentation

Every compact convex body has a uniform linear boundary-strip constant.

theorem exists_convex_boundary_strip_constant {K : Set V}
    (hKc : IsCompact K) (hK : Convex ℝ K) (hKi : (interior K).Nonempty) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (v : V), ‖v‖ ≤ 1 → ∀ h : ℝ, 0 ≤ h →
      μ.real {x | x ∈ K ∧ x + h • v ∉ K} ≤ C * h := by
…