SourceFrozenCenteredCoefficient.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Freezing a selector commutes with the actual physical centered coefficient. This is an identity of totalized integrals, so no extra integrability or boundary-level hypothesis is needed.

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozenProfile_physicalCoefficient line 19
theorem OAI.LipschitzHilbert.SourceLatticePacket.frozenProfile_physicalCenteredWave line 31

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozenProfile_physicalCenteredCoefficient line 41

Source documentation

The frozen selector contributes its conjugate to the analyzing coefficient, including when it is zero and on cutoff boundaries.

theorem frozenProfile_physicalCenteredCoefficient (s t : ℝ) (d : Fin N → ℝ)
    (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (j : Fin N) (u : ι j) (k : κ) :
    (P.frozenProfile c hc).physicalCenteredCoefficient s t d v g j u k =
      conj (c j u k)*P.physicalCenteredCoefficient s t d v g j u k := by
…

Mentions: OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredCoefficient

theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredMaskedBand_eq_frozen line 64

Source documentation

The centered masked band is the original alternate synthesis with the genuine centered coefficient of the frozen analyzing packet.

theorem physicalCenteredMaskedBand_eq_frozen
    (alt : ∀ j, ι j → κ → SchwartzMap (ℝ×ℝ) ℂ)
    (hAlt : ∀ j u k, planarProfileConstant (alt j u k) (2*P.order) ≤ P.profileBound)
    (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
    (T : ∀ j, ι j → SlopeBox) (L A t y : ℝ) (j : Fin N) (x : ℝ) :
    P.physicalCenteredMaskedBand c alt hAlt d v g T L A t y j x =
      WithLp.toLp 2 (fun k => ∑ u : ι j,
        (P.frozenProfile c hc).physicalCenteredCoefficient t t d v g j u k*
          ((T j u).mask L A (x,y+t*x):ℂ)*
          (P.withProfile alt hAlt).physicalPacket t j u k (x,y+t*x)) := by
…

Mentions: OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SourceLatticePacket.physicalCenteredCoefficient, OAI.LipschitzHilbert.SourceLatticePacket.physicalPacket