FarSlabGeometry.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Local strips in the reference coordinates, and the coordinate bounds needed to compare their overlap with a transverse line through a small selected rectangle.

def OAI.LipschitzHilbert.Rectangle.stripSlab line 13
theorem OAI.LipschitzHilbert.Rectangle.mem_stripSlab line 17
theorem OAI.LipschitzHilbert.Rectangle.isCompact_stripSlab line 24
theorem OAI.LipschitzHilbert.Rectangle.volume_stripSlab line 41
theorem OAI.LipschitzHilbert.Rectangle.transverse_coordinate_change_bound line 47

theorem OAI.LipschitzHilbert.Rectangle.short_to_long_slab_coordinates line 68

Source documentation

Coordinate bounds at every point of a short rectangle meeting the fourfold reference interval. The long rectangle meets the original interval.

theorem short_to_long_slab_coordinates (S R T : Rectangle) (c l θ : ℝ)
    (hl : 0 < l) (hθ : 0 < θ) (hθsmall : θ ≤ 1/20)
    (hRlong : 8*l ≤ R.long) (hTlong : T.long ≤ l)
    (hSshort : S.short ≤ θ*l) (hTshort : T.short ≤ θ*l)
    (hRangle : dist (S.axes 0) (R.axes 0) ≤ 2*θ)
    (hTangle : dist (S.axes 0) (T.axes 0) ≤ 2*θ)
    (hR : (R.carrier ∩ S.stripSlab c l).Nonempty)
    (hT : (T.carrier ∩ S.stripSlab c (4*l)).Nonempty)
    {x : Plane} (hx : x ∈ T.carrier) :
    |R.axes.repr (x-R.center) 0| ≤ 32*R.long ∧
      |R.axes.repr (x-R.center) 1| ≤ R.short/2+8*(2*θ*l) := by
…

Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane

theorem OAI.LipschitzHilbert.Rectangle.comparable_slab_coordinates line 123

Source documentation

Comparable lengths permit the same transverse line argument with a larger line radius.

theorem comparable_slab_coordinates (S R T : Rectangle) (c l θ : ℝ)
    (hl : 0 < l) (hθ : 0 < θ) (hθsmall : θ ≤ 1/20)
    (hRlong : l ≤ R.long) (hTlong : T.long ≤ 16*l)
    (hSshort : S.short ≤ θ*l) (hTshort : T.short ≤ θ*l)
    (hRangle : dist (S.axes 0) (R.axes 0) ≤ 2*θ)
    (hTangle : dist (S.axes 0) (T.axes 0) ≤ 2*θ)
    (hR : (R.carrier ∩ S.stripSlab c l).Nonempty)
    (hT : (T.carrier ∩ S.stripSlab c (4*l)).Nonempty)
    {x : Plane} (hx : x ∈ T.carrier) :
    |R.axes.repr (x-R.center) 0| ≤ 64*R.long ∧
      |R.axes.repr (x-R.center) 1| ≤ R.short/2+8*(16*θ*l) := by
…

Mentions: OAI.LipschitzHilbert.Rectangle, OAI.LipschitzHilbert.Plane