OAI/Analysis/LipschitzHilbert/Geometry/FarSelectionGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Geometric consequences of actual maximal non-removal for far pairs. In particular, both widths are small relative to the angle and all remaining angles satisfy the bound needed for popularity projection.

  1. theorem OAI.LipschitzHilbert.Rectangle.dilate_carrier_mono line 16
  2. theorem OAI.LipschitzHilbert.selectionThreshold_small line 30
  3. theorem OAI.LipschitzHilbert.far_selected_earlier_width line 35
  4. theorem OAI.LipschitzHilbert.far_selected_angle_bound line 54
  5. theorem OAI.LipschitzHilbert.far_selected_reference_width line 83

    Source documentation

    Non-removal controls the reference width by the later length as well. This is the local scale bound used in the strip estimates.

    theorem far_selected_reference_width {ι κ : Type*} [Fintype κ]
    (e : κ → Plane ≃ᵐ (ℝ × ℝ)) (R : ι → Rectangle) (previous : Finset ι)
    (s r : ι) (hs : s ∈ previous) (hL : (R r).long ≤ (R s).long)
    (hinter : ((R s).carrier ∩ (R r).carrier).Nonempty)
    (hfar : 64*(R r).short < (R r).long * dist ((R s).axes 0) ((R r).axes 0))
    (hnot : ¬maximalBlocked e R selectionDilation (by norm_num) selectionThreshold previous r) :
    32*(R s).short < (R r).long*dist ((R s).axes 0) ((R r).axes 0) := by
…

    Mentions: OAI.LipschitzHilbert.Plane, OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.maximalBlocked, OAI.LipschitzHilbert.selectionDilation, OAI.LipschitzHilbert.selectionThreshold