DemodulatedCharacter.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact cancellation of the Poisson modulation

The modulation of a unitary field and its inverse has scalar frequency two. The Cauchy character formula therefore cancels the two demodulating factors exactly. This is proved for the actual vector-defined averages.

theorem OAI.KadisonKastler.demodulation_scalar_cancel line 19
theorem OAI.KadisonKastler.measurablePoissonAverage_congr_ae line 40

theorem OAI.KadisonKastler.measurablePoissonAverage_phase_cancel line 57

Source documentation

Cancellation for any bounded measurable field agreeing with the frequency-two character almost everywhere.

theorem measurablePoissonAverage_phase_cancel
    (F : ℝ → H →L[ℂ] H)
    (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) volume)
    (C : ℝ) (hC : ∀ᵐ s, ‖F s‖ ≤ C)
    (hFchar : ∀ᵐ s, F s = poissonCharacterField 2 s)
    (t r : ℝ) (hr : 0 < r) :
    (((Real.exp r : ℂ) * star (Circle.exp t : ℂ)) ^ 2) •
      measurablePoissonAverage F hF C hC t r hr = 1 := by
…

Mentions: OAI.KadisonKastler.poissonCharacterField, OAI.KadisonKastler.measurablePoissonAverage

theorem OAI.KadisonKastler.modulatedUnitaryField_mul_inverse line 74
Source documentation
The pointwise identity behind inverse comparison, for an arbitrary unitary field without continuity assumptions.
```
theorem modulatedUnitaryField_mul_inverse (W : ℝ → unitary (H →L[ℂ] H)) (s : ℝ) :
    modulatedUnitaryField W s * modulatedUnitaryField (fun t => star (W t)) s =
      poissonCharacterField 2 s := by
…
```
Mentions: OAI.KadisonKastler.modulatedUnitaryField, OAI.KadisonKastler.poissonCharacterField