SourceWhitneyPacking.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative packing of the actual Whitney intervals used in the ordinary tree estimate. Bounds are on arbitrary finite subfamilies and therefore also support subsequent monotone summation.

theorem OAI.LipschitzHilbert.SourceWhitney.cell_subset_top_enlargement line 16

Source documentation

A parent witness locates the entire Whitney cell near the horizontal top.

theorem cell_subset_top_enlargement {ι : Type*} (tiles : Finset ι)
    (x ell : ι → ℝ) {c L : ℝ}
    (hcenters : ∀ i ∈ tiles, |x i-c| ≤ L/2) {k j : ℤ}
    (h : Whitney tiles x ell k j) :
    cell 0 k j ⊆ Icc (c-(4*scale k+L/2)) (c+(4*scale k+L/2)) := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney

theorem OAI.LipschitzHilbert.SourceWhitney.finite_length_budget line 31

Source documentation

A finite subfamily with lengths at most r has total length at most 8r+L, where the tile centers lie in an interval of length L.

theorem finite_length_budget {ι : Type*} (tiles : Finset ι)
    (x ell : ι → ℝ) {c L r : ℝ} (hL : 0 ≤ L) (hr : 0 ≤ r)
    (hcenters : ∀ i ∈ tiles, |x i-c| ≤ L/2)
    (S : Finset (ℤ×ℤ))
    (hW : ∀ p ∈ S, Whitney tiles x ell p.1 p.2)
    (hscale : ∀ p ∈ S, scale p.1 ≤ r) :
    ∑ p ∈ S, scale p.1 ≤ 8*r+L := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney

theorem OAI.LipschitzHilbert.SourceWhitney.small_length_budget line 64

Source documentation

The small Whitney cells have a summable total length controlled by the top length.

theorem small_length_budget {ι : Type*} (tiles : Finset ι)
    (x ell : ι → ℝ) {c L : ℝ} (hL : 0 ≤ L)
    (hcenters : ∀ i ∈ tiles, |x i-c| ≤ L/2)
    (S : Finset (ℤ×ℤ))
    (hW : ∀ p ∈ S, Whitney tiles x ell p.1 p.2)
    (hscale : ∀ p ∈ S, scale p.1 ≤ L) :
    ∑ p ∈ S, scale p.1 ≤ 9*L := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney

theorem OAI.LipschitzHilbert.SourceWhitney.large_scale_card line 76

Source documentation

At each length larger than the top there are at most nine Whitney cells. This is the multiplicity needed for the geometric tail.

theorem large_scale_card {ι : Type*} (tiles : Finset ι)
    (x ell : ι → ℝ) {c L : ℝ} (hL : 0 ≤ L)
    (hcenters : ∀ i ∈ tiles, |x i-c| ≤ L/2) (k : ℤ) (hk : L ≤ scale k)
    (J : Finset ℤ) (hW : ∀ j ∈ J, Whitney tiles x ell k j) :
    J.card ≤ 9 := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney