OAI/Analysis/LipschitzHilbert/Estimates/WitnessInterval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.SlopeBox.witnessInterval line 14
2. theorem OAI.LipschitzHilbert.SlopeBox.horizontal_distance_le_radius line 17
3. theorem OAI.LipschitzHilbert.SlopeBox.mem_witnessInterval line 26
4. theorem OAI.LipschitzHilbert.SlopeBox.witnessInterval_length line 33
5. theorem OAI.LipschitzHilbert.SlopeBox.witness_centered_line_average line 40

   Source documentation

   The witness produces the required average on a concrete interval that also contains the evaluation point, with no further interval selection.

   theorem witness_centered_line_average (T : SlopeBox) (E : Set (ℝ × ℝ)) (hE : IsCompact E)
       {A q P : ℝ} (hA : 0 < A) (hq : 0 ≤ q) (hP : 0 < P) (hAP : A ≤ 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 : ℝ × ℝ)
       (hz : T.radius z ≤ P) (bin : Set ℝ) (hbin : MeasurableSet bin)
       (htransfer : ∀ w ∈ E, u (referencePoint s z w) ∈ bin) :
       z.1 ∈ T.witnessInterval P ∧
         q / (4 * A * P) ≤
           (∫ x in T.witnessInterval P, (LipschitzHilbert.lineBinSet u s z bin).indicator
             (fun _ => (1 : ℝ)) x) / volume.real (T.witnessInterval P) := by
   …

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