WitnessLineAverage.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The compact transferred witness gives the required popular line bin.

def OAI.LipschitzHilbert.linePoint line 14
def OAI.LipschitzHilbert.lineBinSet line 17
theorem OAI.LipschitzHilbert.measurableSet_lineBinSet line 20
theorem OAI.LipschitzHilbert.witness_projection_subset_lineBin line 28
Source documentation
A transferred witness has its entire horizontal projection inside the same measurable line bin.
```
theorem witness_projection_subset_lineBin (E : Set (ℝ × ℝ))
    (u : ℝ × ℝ → ℝ) (s : ℝ) (z : ℝ × ℝ) (bin : Set ℝ)
    (htransfer : ∀ w ∈ E, u (SlopeBox.referencePoint s z w) ∈ bin) :
    Prod.fst '' E ⊆ lineBinSet u s z bin := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox.referencePoint, OAI.LipschitzHilbert.lineBinSet

theorem OAI.LipschitzHilbert.SlopeBox.witness_line_integral line 39

Source documentation

Turning the geometric transfer into an integral lower bound requires only the measurable bin and the actual compact witness.

theorem witness_line_integral (T : SlopeBox) (E : Set (ℝ × ℝ)) (hE : IsCompact E)
    {A q : ℝ} (hA : 0 < A) (hbox : ∀ w ∈ E, T.radius w ≤ A)
    (harea : q * T.length * T.width ≤ (volume.prod volume).real E)
    (u : ℝ × ℝ → ℝ) (hu : Measurable u) (s : ℝ) (z : ℝ × ℝ)
    (bin I : Set ℝ) (hbin : MeasurableSet bin) (hIfinite : volume I ≠ ∞)
    (hproj : ∀ w ∈ E, w.1 ∈ I)
    (htransfer : ∀ w ∈ E, u (referencePoint s z w) ∈ bin) :
    q * T.length / (2 * A) ≤
      ∫ x in I, (lineBinSet u s z bin).indicator (fun _ => (1 : ℝ)) x := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.referencePoint, OAI.LipschitzHilbert.lineBinSet

theorem OAI.LipschitzHilbert.SlopeBox.witness_line_average line 60

Source documentation

The popular-bin threshold is the witness fraction divided only by the fixed geometric dilation factors.

theorem witness_line_average (T : SlopeBox) (E : Set (ℝ × ℝ)) (hE : IsCompact E)
    {A q P : ℝ} (hA : 0 < A) (hq : 0 ≤ q) (hP : 0 < P)
    (hbox : ∀ w ∈ E, T.radius w ≤ A)
    (harea : q * T.length * T.width ≤ (volume.prod volume).real E)
    (u : ℝ × ℝ → ℝ) (hu : Measurable u) (s : ℝ) (z : ℝ × ℝ)
    (bin I : Set ℝ) (hbin : MeasurableSet bin) (hIfinite : volume I ≠ ∞)
    (hIpos : 0 < volume.real I) (hIlength : volume.real I ≤ P * T.length)
    (hproj : ∀ w ∈ E, w.1 ∈ I)
    (htransfer : ∀ w ∈ E, u (referencePoint s z w) ∈ bin) :
    q / (2 * A * P) ≤
      (∫ x in I, (lineBinSet u s z bin).indicator (fun _ => (1 : ℝ)) x) / volume.real I := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.referencePoint, OAI.LipschitzHilbert.lineBinSet