OAI/Analysis/KadisonKastler/DemodulatedPoisson.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual demodulated smoothing fields

These are the fields used before polar decomposition. An essential bound on the boundary, or an essential comparison with the modulated modular unitaries, passes to a uniform norm bound at every positive height.

  1. def OAI.KadisonKastler.demodulatedPoissonAverage line 21
  2. theorem OAI.KadisonKastler.norm_demodulation_scalar line 27
  3. theorem OAI.KadisonKastler.norm_demodulatedPoissonAverage_le line 33
  4. theorem OAI.KadisonKastler.continuous_demodulatedPoissonAverage line 42
  5. theorem OAI.KadisonKastler.norm_demodulatedPoissonAverage_sub_boundary_le line 52

    Source documentation

    The comparison holds at every time, even when the boundary estimates hold only almost everywhere.

    theorem norm_demodulatedPoissonAverage_sub_boundary_le
    (F : ℝ → H →L[ℂ] H) (hF : ∀ x, AEStronglyMeasurable (fun s => F s x) volume)
    (C : ℝ) (hC : ∀ᵐ s, ‖F s‖ ≤ C)
    (W : ℝ → unitary (H →L[ℂ] H))
    (hW : ∀ x, Continuous (fun t => (W t : H →L[ℂ] H) x))
    {δ : ℝ} (hδ : 0 ≤ δ) (hFW : ∀ᵐ s, ‖F s - modulatedUnitaryField W s‖ ≤ δ)
    (t r : ℝ) (hr : 0 < r) :
    ‖demodulatedPoissonAverage F hF C hC t r hr - poissonBoundaryApprox W hW t r‖ ≤
      Real.exp r * δ := by
…

    Mentions: OAI.KadisonKastler.modulatedUnitaryField, OAI.KadisonKastler.demodulatedPoissonAverage, OAI.KadisonKastler.poissonBoundaryApprox