SourceShortTreeSum.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Summation of the short-tree density tails over the actual center lattice and all retained dyadic scales.

theorem OAI.LipschitzHilbert.SourceWhitney.sheared_strip_kernel_sum line 13

Source documentation

A single length, with the actual sheared lattice and strip cutoff.

theorem sheared_strip_kernel_sum (a b ell W delta c y r : ℝ)
    (hell : 0<ell) (hW : 0<W) (S : Finset (ℤ×ℤ))
    (hstrip : ∀ p∈S, |b+delta*ell*p.1+W*p.2-y|≤W)
    (hsep : ∀ p∈S, ell≤r → r≤stripDistance c r (a+ell*p.1)) :
    (∑ p∈S, (1+(stripDistance c r (a+ell*p.1)/ell)^2)⁻¹^2) ≤
      144*(4*Real.pi)^2 := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.stripDistance

theorem OAI.LipschitzHilbert.SourceWhitney.sheared_strip_kernel_decay_sum line 28

Source documentation

A single short length retains the squared length-to-distance gain.

theorem sheared_strip_kernel_decay_sum (a b ell W delta c y r : ℝ)
    (hell : 0<ell) (hW : 0<W) (hr : 0<r) (S : Finset (ℤ×ℤ))
    (hstrip : ∀ p∈S, |b+delta*ell*p.1+W*p.2-y|≤W)
    (hsep : ∀ p∈S, r≤stripDistance c r (a+ell*p.1)) :
    (∑ p∈S, (1+(stripDistance c r (a+ell*p.1)/ell)^2)⁻¹^2) ≤
      144*(4*Real.pi)^2*(ell/r)^2 := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.stripDistance

theorem OAI.LipschitzHilbert.SourceWhitney.short_lattice_sum line 46

Source documentation

The weighted short-packet tail on one Whitney strip, summed over all retained sites and all lengths at most R, is bounded by its strip scale.

theorem short_lattice_sum (L R W c y r : ℝ) (hL : 0<L) (hR : 0≤R) (hW : 0<W)
    (levels : Finset ℕ) (sites : ℕ → Finset (ℤ×ℤ)) (a b delta : ℕ → ℝ)
    (hlength : ∀ j∈levels, L/(2:ℝ)^j≤R)
    (hstrip : ∀ j∈levels, ∀ p∈sites j,
      |b j+delta j*(L/(2:ℝ)^j)*p.1+W*p.2-y|≤W)
    (hsep : ∀ j∈levels, ∀ p∈sites j, L/(2:ℝ)^j≤r →
      r≤stripDistance c r (a j+(L/(2:ℝ)^j)*p.1)) :
    (∑ j∈levels, ∑ p∈sites j, (L/(2:ℝ)^j)*W*
      (1+(stripDistance c r (a j+(L/(2:ℝ)^j)*p.1)/(L/(2:ℝ)^j))^2)⁻¹^2) ≤
      288*(4*Real.pi)^2*W*R := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.stripDistance

theorem OAI.LipschitzHilbert.SourceWhitney.short_lattice_decay_sum line 76

Source documentation

Outside the top length, the same sum retains quadratic decay in the Whitney length. This is summable over the large Whitney cells.

theorem short_lattice_decay_sum (L R W c y r : ℝ)
    (hL : 0<L) (hR : 0≤R) (hW : 0<W) (hr : 0<r)
    (levels : Finset ℕ) (sites : ℕ → Finset (ℤ×ℤ)) (a b delta : ℕ → ℝ)
    (hlength : ∀ j∈levels, L/(2:ℝ)^j≤R)
    (hstrip : ∀ j∈levels, ∀ p∈sites j,
      |b j+delta j*(L/(2:ℝ)^j)*p.1+W*p.2-y|≤W)
    (hsep : ∀ j∈levels, ∀ p∈sites j,
      r≤stripDistance c r (a j+(L/(2:ℝ)^j)*p.1)) :
    (∑ j∈levels, ∑ p∈sites j, (L/(2:ℝ)^j)*W*
      (1+(stripDistance c r (a j+(L/(2:ℝ)^j)*p.1)/(L/(2:ℝ)^j))^2)⁻¹^2) ≤
      288*(4*Real.pi)^2*W*R*(R/r)^2 := by
…

Mentions: OAI.LipschitzHilbert.SourceWhitney.stripDistance