SourceMaskedPhysicalMoments.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Physical shortness and the narrow reference cone discharge the mask-rate hypotheses. The resulting masked mixed moments use the original integral coefficients and actual top masks.

theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalReferenceMaskRate line 18

theorem OAI.LipschitzHilbert.SourceLatticePacket.masked_mixed_reference_uniform_moments line 32

Source documentation

All constants precede the finite packet family, masks, and root window. No derivative or Fourier premise is imposed on the masks.

theorem masked_mixed_reference_uniform_moments (hVariation : LepingleInput)
    {lo hi : ℝ} (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ B M : ℝ, 0 < B ∧ 0 < M ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
      (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
      (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.frozenProfile c hc).raw 0 j u k y) xi = 0) →
…

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