SourceWhitneySummation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Summation of the local short-tree bounds over the Whitney partition: total small-cell length and the large-cell geometric tail.

theorem OAI.LipschitzHilbert.SourceWhitney.large_whitney_ratio_sum line 16

Source documentation

Summing the far-strip decay over the large Whitney intervals costs only an absolute factor, including all possible integer scales.

theorem large_whitney_ratio_sum {ι : 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)
    (hlarge : ∀ p∈S, L≤scale p.1) :
    (∑ p∈S, (L/scale p.1)^2) ≤ 18 := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney

def OAI.LipschitzHilbert.SourceWhitney.shortWhitneyWeight line 58

theorem OAI.LipschitzHilbert.SourceWhitney.short_whitney_weight_sum line 62

Source documentation

The small-cell contribution and large-cell tail together have total weight at most 27L.

theorem short_whitney_weight_sum {ι : 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) :
    (∑ p∈S, shortWhitneyWeight L (scale p.1)) ≤ 27*L := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney, OAI.LipschitzHilbert.SourceWhitney.shortWhitneyWeight

theorem OAI.LipschitzHilbert.SourceWhitney.sum_short_strip_bounds line 84

Source documentation

Local strip estimates with the manuscript's two decay regimes sum to the required top-area bound.

theorem sum_short_strip_bounds {ι : Type*} (tiles : Finset ι)
    (x ell : ι → ℝ) {c L W A : ℝ} (hL : 0<L) (hW : 0≤W) (hA : 0≤A)
    (hcenters : ∀ i∈tiles, |x i-c|≤L/2) (S : Finset (ℤ×ℤ))
    (hWhitney : ∀ p∈S, Whitney tiles x ell p.1 p.2) (mass : ℤ×ℤ → ℝ)
    (hsmall : ∀ p∈S, scale p.1≤L → mass p≤A*W*scale p.1)
    (hlarge : ∀ p∈S, L<scale p.1 → mass p≤A*W*L*(L/scale p.1)^2) :
    (∑ p∈S, mass p) ≤ 27*A*L*W := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.Whitney