SourceMixedReference.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Reference moments with distinct analyzing and synthesizing profiles. The selector is frozen only in the analyzing coefficient; it is not multiplied into the synthesis a second time.

def OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine line 24
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine_coeff line 29
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine_wave line 34
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine_budget_iff line 38
def OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceBand line 45
Source documentation
The actual mixed synthesis band, with the original integral coefficient and no repeated frozen selector in the synthesis profile.
```
def mixedReferenceBand (j : Fin N) (y x : ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine_partial line 50
theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceBand_variation line 71

theorem OAI.LipschitzHilbert.SourceLatticePacket.mixed_reference_uniform_moments line 88

Source documentation

Independent profile choices share the same normalized coefficient budget, and both reference moments remain uniform in dimension and scale.

theorem mixed_reference_uniform_moments (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ A M : ℝ, 0 < A ∧ 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