RegularPacketFubini.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the packet reconstruction kernel

An integrable weight in the packet variables and a translated L² square give an integrable three-variable majorant. This justifies the Fubini interchange in the finite packet reconstruction without assuming bounded representatives of the Hilbert-space vectors.

theorem OAI.KadisonKastler.integrable_weighted_translate line 20

theorem OAI.KadisonKastler.integrable_regularPacket_kernel line 55

Source documentation

The complete scalar kernel is integrable over the two packet variables and the translation variable.

theorem integrable_regularPacket_kernel
    (φ ψ : ℝ → ℂ) (hφ : Integrable φ volume) (hψ : Integrable ψ volume)
    (A : H →L[ℂ] H) (f g : RegularCoreHilbert H) :
    Integrable (fun p : (ℝ × ℝ) × ℝ =>
      (φ p.1.1 * star (ψ p.1.2)) *
        inner ℂ ((U (Multiplicative.ofAdd p.1.1) : H →L[ℂ] H) (f (p.2 + p.1.1)))
          (A ((U (Multiplicative.ofAdd p.1.2) : H →L[ℂ] H) (g (p.2 + p.1.2)))))
      (((volume : Measure ℝ).prod volume).prod volume) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert