SourceReferenceMoments.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Reference-line packets are normalized at their actual horizontal length before applying the published scalar variation input. The local coefficient budget is independent of that length, the number of scales, and the Hilbert dimension.

def OAI.LipschitzHilbert.SourceLatticePacket.referencePlanarFamily line 22
theorem OAI.LipschitzHilbert.SourceLatticePacket.family_derivative line 25
theorem OAI.LipschitzHilbert.SourceLatticePacket.referencePlanarFamily_derivative line 37
def OAI.LipschitzHilbert.SourceLatticePacket.referenceAnalyzedLine line 58
theorem OAI.LipschitzHilbert.SourceLatticePacket.referenceAnalyzedLine_coeff line 66
theorem OAI.LipschitzHilbert.SourceLatticePacket.referenceAnalyzedLine_wave line 74
theorem OAI.LipschitzHilbert.SourceLatticePacket.referenceAnalyzedLine_topLength line 78
theorem OAI.LipschitzHilbert.SourceLatticePacket.referencePlanarFamily_cutoffs line 85

theorem OAI.LipschitzHilbert.SourceLatticePacket.referenceAnalyzedLine_uniform_budget line 106

Source documentation

The normalized analyzing coefficients have a single budget chosen before the packet family, length and dimension.

theorem referenceAnalyzedLine_uniform_budget (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ A : ℝ, 0 < A ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1),
      Monotone d →
      (∀ j u k y xi, |xi| < (lo/P.topLength)*(2:ℝ)^j.val → 𝓕 (P.raw 0 j u k y) xi = 0) →
      (∀ j u k y xi, (hi/P.topLength)*(2:ℝ)^j.val < |xi| → 𝓕 (P.raw 0 j u k y) xi = 0) →
      ∀ y, (P.referenceAnalyzedLine d v hv g hg hg1 y).HasLocalBudget (A/Real.pi^4) := by
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket