SourceMaskedSynthesis.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The masked reference family synthesizes the original physical top mask and alternate packet. Its analyzing coefficient is unchanged, so the normalization is the original constant * pi^2, not its doubled synthesis-envelope constant.

theorem OAI.LipschitzHilbert.SourceLatticePacket.mixedReferenceLine_length line 25
theorem OAI.LipschitzHilbert.SourceLatticePacket.normalized_mask_rate line 34
def OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine line 52
Source documentation
The actual top mask is applied only to the synthesis wave.
```
def maskedMixedReferenceLine
    (hrate : ∀ j u, 2*(⌈L⌉₊:ℝ)*
      (|(T j u).maskLineA L A|+|(T j u).maskLineC L A t|) ≤ 1/P.length j) :
    LinePacketFamily N κ ι :=
…
```
Mentions: OAI.LipschitzHilbert.LinePacketFamily
theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine_coeff line 66
theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine_wave line 71
theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine_budget_iff line 78
def OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceBand line 85
Source documentation
The exact physical band, with the original analyzing coefficient, the physical top mask, and the original alternate synthesis packet.
```
def maskedMixedReferenceBand (j : Fin N) (x : ℝ) : EuclideanSpace ℂ κ :=
…
```
theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceLine_partial line 90
theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceBand_variation line 112

theorem OAI.LipschitzHilbert.SourceLatticePacket.maskedMixedReferenceBand_physical line 131

Source documentation

In physical coordinates the frozen selector appears exactly once, conjugated in the original analyzing coefficient. The synthesis packet and its mask are the original physical ones.

theorem maskedMixedReferenceBand_physical (j : Fin N) (x : ℝ) :
    P.maskedMixedReferenceBand c hc alt hAlt d
      (fun z => v (sourceReferenceToPhysical t z))
      (fun z => g (sourceReferenceToPhysical t z)) T L A t y j x =
      WithLp.toLp 2 (fun k => ∑ u : ι j,
        (conj (c j u k)*P.physicalCoefficient 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.sourceReferenceToPhysical, OAI.LipschitzHilbert.SourceLatticePacket.physicalPacket