SourceShortTreeOverlap.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The short-tree summation uses actual distance to the Whitney strip, actual sheared center lattices, and a finite dyadic length sum.

def OAI.LipschitzHilbert.SourceWhitney.stripDistance line 16
theorem OAI.LipschitzHilbert.SourceWhitney.stripDistance_nonneg line 18
theorem OAI.LipschitzHilbert.SourceWhitney.center_distance_le line 20
theorem OAI.LipschitzHilbert.SourceWhitney.stripDistance_le_point line 25
theorem OAI.LipschitzHilbert.SourceWhitney.stripDistance_large line 33
theorem OAI.LipschitzHilbert.SourceWhitney.inverse_quadratic_le_center line 42
Source documentation
An interval-distance kernel is controlled by a center kernel once the center distance is at most twice that distance plus one packet length.
```
theorem inverse_quadratic_le_center {s c ell d : ℝ} (hell : 0<ell) (hd : 0≤d)
    (hc : |s-c|≤2*d+ell) :
    (1+(d/ell)^2)⁻¹ ≤ 8*lineEnvelope s ell 1 c := by
…
```
Mentions: OAI.LipschitzHilbert.lineEnvelope
theorem OAI.LipschitzHilbert.SourceWhitney.strip_kernel_le_center line 62
theorem OAI.LipschitzHilbert.SourceWhitney.strip_kernel_le_center_decay line 85
theorem OAI.LipschitzHilbert.SourceWhitney.sheared_strip_overlap line 112
Source documentation
A sheared lattice with centers in a strip has uniformly bounded horizontal envelope sum, without a tile-cardinality factor.
```
theorem sheared_strip_overlap (a b ell W delta c y : ℝ)
    (hell : 0<ell) (hW : 0<W) (S : Finset (ℤ×ℤ))
    (hstrip : ∀ p∈S, |b+delta*ell*p.1+W*p.2-y|≤W) :
    (∑ p∈S, lineEnvelope (a+ell*p.1) ell 1 c) ≤ 18*(4*Real.pi)^2 := by
…
```
Mentions: OAI.LipschitzHilbert.lineEnvelope