RegularConvolutionCoefficients.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Coefficients of the factored convolution operators

These formulas express the constructed action integrals as actual single and double scalar integrals. They are the comparison formulas for Haar averages of finite packet matrices.

theorem OAI.KadisonKastler.integral_inner_left line 21
theorem OAI.KadisonKastler.integrable_star_weight line 31
theorem OAI.KadisonKastler.regularAction_adjoint line 41
theorem OAI.KadisonKastler.integrable_action_vector line 52

theorem OAI.KadisonKastler.inner_regularActionIntegral line 66

Source documentation

A coefficient of the action integral, with its adjoint moved to the test vector.

theorem inner_regularActionIntegral
    (w : ℝ → ℂ) (hw : Integrable w volume) (f g : RegularCoreHilbert H) :
    inner ℂ f (regularActionIntegral U hU w hw g) =
      ∫ t : ℝ, w t * inner ℂ
        ((regularCoreAction U (Multiplicative.ofAdd t) :
          RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) f) g := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularActionIntegral, OAI.KadisonKastler.regularCoreAction

theorem OAI.KadisonKastler.regularActionIntegral_star_apply line 92

Source documentation

The adjoint action integral has the positive-translation formula.

theorem regularActionIntegral_star_apply
    (w : ℝ → ℂ) (hw : Integrable w volume) (g : RegularCoreHilbert H) :
    star (regularActionIntegral U hU w hw) g =
      ∫ t : ℝ, star (w t) •
        (regularCoreAction U (Multiplicative.ofAdd t) :
          RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) g := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularActionIntegral, OAI.KadisonKastler.regularCoreAction

theorem OAI.KadisonKastler.inner_regularPacketConvolution line 131

Source documentation

The two scalar weights and the constant operator are the exact double-integral kernel of the factored packet convolution.

theorem inner_regularPacketConvolution
    (φ ψ : ℝ → ℂ) (hφ : Integrable φ volume) (hψ : Integrable ψ volume)
    (A : H →L[ℂ] H) (f g : RegularCoreHilbert H) :
    inner ℂ f (regularPacketConvolution U hU φ ψ hφ hψ A g) =
      ∫ q : ℝ, φ q * (∫ u : ℝ, star (ψ u) *
        inner ℂ ((regularCoreAction U (Multiplicative.ofAdd q) :
          RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) f)
          (regularConstantHom (volume : Measure ℝ) A
            ((regularCoreAction U (Multiplicative.ofAdd u) :
              RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H) g))) := by
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularPacketConvolution, OAI.KadisonKastler.regularCoreAction, OAI.KadisonKastler.regularConstantHom