FarSlabLineSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The long-rectangle contribution over a local reference strip is bounded by the actual line part of the auxiliary maximal operator.

theorem OAI.LipschitzHilbert.Rectangle.slab_intersection_transverse line 13
theorem OAI.LipschitzHilbert.Rectangle.slab_intersection_min_area line 40
theorem OAI.LipschitzHilbert.far_slab_line_sum line 84

theorem OAI.LipschitzHilbert.comparable_slab_line_sum line 162

Source documentation

The comparable-length version uses the same fixed direction net.

theorem comparable_slab_line_sum (D : κ → Rectangle) (R : ι → Rectangle)
    (s : Finset ι) (S T : Rectangle) (i : κ) (c l θ : ℝ)
    (hl : 0 < l) (hθ : 0 < θ) (hθsmall : θ ≤ 1/20)
    (hRlong : ∀ j ∈ s, l ≤ (R j).long) (hTlong : T.long ≤ 16*l)
    (hSshort : S.short ≤ θ*l) (hTshort : T.short ≤ θ*l)
    (hRangle : ∀ j ∈ s, dist (S.axes 0) ((R j).axes 0) ≤ 2*θ)
    (hRlower : ∀ j ∈ s, θ/2 ≤ dist (S.axes 0) ((R j).axes 0))
    (hTangle : dist (S.axes 0) (T.axes 0) ≤ 2*θ)
    (hR : ∀ j ∈ s, ((R j).carrier ∩ S.stripSlab c l).Nonempty)
    (hT : (T.carrier ∩ S.stripSlab c (4*l)).Nonempty)
    (htrans : ∀ j ∈ s, 1/2 ≤ |(R j).axes.repr ((D i).axes 0) 1|)
    (x : Plane) (hx : x ∈ T.carrier) :
…

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