OAI/Analysis/LipschitzHilbert/Geometry/SelectedFarFamily.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A finite far family inside an actual selection run. These data will be obtained from the projected-popularity grouping; the local estimates below use no further geometric assumptions.

  1. structure OAI.LipschitzHilbert.SelectedFarFamily line 15
  2. abbrev OAI.LipschitzHilbert.SelectedFarFamily.refRect line 43
  3. def OAI.LipschitzHilbert.SelectedFarFamily.longMembers line 45
  4. def OAI.LipschitzHilbert.SelectedFarFamily.comparableMembers line 48
  5. theorem OAI.LipschitzHilbert.SelectedFarFamily.comparable_mass line 51
  6. theorem OAI.LipschitzHilbert.SelectedFarFamily.short_absent line 70

    Source documentation

    A strip with large long-rectangle mass cannot meet a shorter selected rectangle, even in its fourfold enlargement.

    theorem short_absent (F : SelectedFarFamily ι) (c l : ℝ) (hl : 0 < l)
    (hdense : volume (F.refRect.stripSlab c l) ≤
      stripMass F.rectangles (F.longMembers l) F.refRect c l)
    (r : ι) (hr : r ∈ F.members) (hrshort : (F.rectangles r).long < l) :
    ¬((F.rectangles r).carrier ∩ F.refRect.stripSlab c (4*l)).Nonempty := by
…

    Mentions: OAI.LipschitzHilbert.SelectedFarFamily, OAI.LipschitzHilbert.stripMass