SourceTransverseTail.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The remaining transverse tail in the long-tree density estimate: 412 powers in squared energy absorb twice the density loss 203, leaving the summable sixth power.

theorem OAI.LipschitzHilbert.summable_transverse_sixth line 15
Source documentation
The transverse tail left by the fixed manuscript exponents is summable.
```
theorem summable_transverse_sixth :
    Summable (fun n : ℤ => ((1+|(n:ℝ)|)^6)⁻¹) := by
…
```
def OAI.LipschitzHilbert.transverseTailConstant line 26
theorem OAI.LipschitzHilbert.transverseTailConstant_nonneg line 28
theorem OAI.LipschitzHilbert.finite_transverse_tail line 31

theorem OAI.LipschitzHilbert.transverse_density_cauchy line 37

Source documentation

Weighted Cauchy--Schwarz with exactly the exponents needed by the cell-density and polynomial-energy estimates.

theorem transverse_density_cauchy {J : Type*} (s : Finset J)
    (A m w : J → ℝ) (hm : ∀ j∈s, 0≤m j) (hw : ∀ j∈s, 0<w j) :
    (∑ j∈s, A j*m j*(w j)^203)^2≤
      (∑ j∈s, (A j)^2*m j*(w j)^412)*(∑ j∈s, m j/(w j)^6) := by
…

theorem OAI.LipschitzHilbert.finite_density_supremum_sum line 57

Source documentation

Density mass times the actual supremum is controlled by weighted energy and the summable volume tail.

theorem finite_density_supremum_sum {J : Type*} (s : Finset J)
    (A d m w : J → ℝ) (D E V : ℝ)
    (hA : ∀ j∈s, 0≤A j) (hd : ∀ j∈s, 0≤d j)
    (hm : ∀ j∈s, 0≤m j) (hw : ∀ j∈s, 0<w j)
    (hE : 0≤E)
    (hmass : ∀ j∈s, d j≤D*(w j)^203*m j)
    (henergy : (∑ j∈s, (A j)^2*m j*(w j)^412)≤E)
    (hvolume : (∑ j∈s, m j/(w j)^6)≤V) :
    (∑ j∈s, A j*d j)^2≤D^2*E*V := by
…

theorem OAI.LipschitzHilbert.SourceWhitney.finite_whitney_transverse_budget line 88

Source documentation

For any finite family of small Whitney intervals, the entire transverse tail has a uniform volume budget.

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

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