RegularPacketAveraging.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Haar averages of finite packet operators

The packet and convolution expressions are the same absolutely integrable three-variable kernel, with the integrations reordered. Thus every averaged packet matrix with a commutant coefficient belongs to the concrete generated commutant algebra.

theorem OAI.KadisonKastler.inner_integrals line 23
theorem OAI.KadisonKastler.integrable_packet_translate line 43
theorem OAI.KadisonKastler.packet_adjoint_translate line 51
theorem OAI.KadisonKastler.action_coefficient_integral line 61

theorem OAI.KadisonKastler.integral_packet_orbit_inner_eq line 82

Source documentation

Haar averaging a packet operator is exactly the constructed convolution with the same commutant coefficient.

theorem integral_packet_orbit_inner_eq
    (φ ψ : Lp ℂ 2 (volume : Measure ℝ))
    (hφ : Integrable φ volume) (hψ : Integrable ψ volume)
    (A : H →L[ℂ] H) (f g : RegularCoreHilbert H) :
    (∫ r : ℝ, inner ℂ
      ((regularGaugedPacket U hU φ).adjoint (regularTranslateApply r f))
      (A ((regularGaugedPacket U hU ψ).adjoint (regularTranslateApply r g)))) =
      inner ℂ f (regularPacketConvolution U hU φ ψ hφ hψ A g) := by
…

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