RegularPacketIntegrals.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Integral formulas for wave-packet compression

The adjoint of a scalar packet is its ordinary vector integral. The gauged formula inserts the original unitary group inside that integral. Both integrability assertions follow from the actual L² bounds.

theorem OAI.KadisonKastler.integrable_scalarPacket_pair line 22
theorem OAI.KadisonKastler.regularTensorVector_adjoint_apply line 32
Source documentation
Scalar packet compression is the usual vector-valued integral.
```
theorem regularTensorVector_adjoint_apply
    (φ : Lp ℂ 2 (volume : Measure ℝ)) (f : RegularCoreHilbert H) :
    (regularTensorVector φ).adjoint f = ∫ t : ℝ, star (φ t) • f t := by
…
```
Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularTensorVector
theorem OAI.KadisonKastler.integrable_gaugedPacket_pair line 49

theorem OAI.KadisonKastler.regularGaugedPacket_adjoint_apply line 59

Source documentation

The adjoint of a gauged packet integrates the untwisted vector field.

theorem regularGaugedPacket_adjoint_apply
    (φ : Lp ℂ 2 (volume : Measure ℝ)) (f : RegularCoreHilbert H) :
    (regularGaugedPacket U hU φ).adjoint f =
      ∫ t : ℝ, star (φ t) • (U (Multiplicative.ofAdd t) : H →L[ℂ] H) (f t) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularGaugedPacket