SourceSupportedMoments.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Empty initial scales impose no lower bound on the reference window. The root moment estimates need only contain the lengths of actual retained packets. This is the situation for the fixed short reference collection in §8.

theorem OAI.LipschitzHilbert.LinePacketFamily.shortPackets_eq_of_supported line 20
theorem OAI.LipschitzHilbert.LinePacketFamily.shortSquare_eq_of_supported line 28
theorem OAI.LipschitzHilbert.LinePacketFamily.root_square_bound_of_supported line 39
theorem OAI.LipschitzHilbert.LinePacketFamily.mean_bound_of_supported line 57
theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_root_integral_of_supported line 91
theorem OAI.LipschitzHilbert.LinePacketFamily.squareSum_mean_of_supported line 106
theorem OAI.LipschitzHilbert.LinePacketFamily.squareFunction_moment_of_supported line 122

theorem OAI.LipschitzHilbert.LinePacketFamily.uniform_line_moment_of_supported line 152

Source documentation

The published-input constant is uniform before choosing the finite packet family. The reference window contains only the retained lengths.

theorem uniform_line_moment_of_supported (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ A : ℝ, 0 < A ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : LinePacketFamily N κ ι) (B : ℝ),
      0 ≤ B → P.HasLocalBudget B →
      (∀ j i k xi, |xi| < lo*(2:ℝ)^j.val → 𝓕 (P.wave j i k) xi = 0) →
      (∀ j i k xi, hi*(2:ℝ)^j.val < |xi| → 𝓕 (P.wave j i k) xi = 0) →
      ∀ (grid : FiniteLineGrid), 1 < grid.branching →
      (∀ j (_u : ι j), P.length j ≤ grid.width) → ∀ p : ℝ, 0 ≤ p →
      (∫⁻ x, (ENNReal.ofReal |P.variation x|)^p ∂grid.lineMeasure) ≤
        (2:ℝ≥0∞)^p*(7*ENNReal.ofReal ((p*(((grid.branching:ℝ)+2)*
          (2*Real.sqrt (A*P.constant^2*B+1)+4*(P.constant*(4*Real.pi)^2)))/
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.LinePacketFamily, OAI.LipschitzHilbert.FiniteLineGrid