OAI/Analysis/LipschitzHilbert/Estimates/CompactWitness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.exists_compact_half_witness line 17

   Source documentation

   Inner regularity produces the compact witness with half the original area, while preserving every pointwise witness condition by inclusion.

   theorem exists_compact_half_witness (E : Set (ℝ × ℝ)) (hE : MeasurableSet E)
       (hfinite : (volume.prod volume) E ≠ ∞) (hpos : 0 < (volume.prod volume).real E) :
       ∃ K ⊆ E, IsCompact K ∧ (volume.prod volume).real E / 2 ≤
         (volume.prod volume).real K := by
   …

2. theorem OAI.LipschitzHilbert.SlopeBox.exists_compact_popularity_witness line 34

   Source documentation

   Extract the compact subwitness needed by the line-average argument from the original measurable popularity witness.

   theorem exists_compact_popularity_witness (T : SlopeBox) (E : Set (ℝ × ℝ))
       (hE : MeasurableSet E) (hfinite : (volume.prod volume) E ≠ ∞) {q A : ℝ}
       (hq : 0 < q) (harea : q * T.length * T.width ≤ (volume.prod volume).real E)
       (hbox : ∀ z ∈ E, T.radius z ≤ A) :
       ∃ K ⊆ E, IsCompact K ∧
         (q / 2) * T.length * T.width ≤ (volume.prod volume).real K ∧
         ∀ z ∈ K, T.radius z ≤ A := by
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox