HardyPoissonProducts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Poisson products from the published Hardy evaluation

The boundary multiplication operators and their positive-frequency algebra are concrete. Multiplicativity is obtained by applying the precisely cited published evaluation homomorphism, including for constant middle factors.

theorem OAI.KadisonKastler.RepresentsOperatorField.mul line 25
theorem OAI.KadisonKastler.RepresentsOperatorField.mem_positiveFrequencyAlgebra line 35
theorem OAI.KadisonKastler.poisson_constant line 46

theorem OAI.KadisonKastler.measurablePoissonAverage_mul_of_hardy line 58

Source documentation

Exact multiplication of Poisson extensions of positive-frequency preserving, bounded measurable multiplication operators.

theorem measurablePoissonAverage_mul_of_hardy
    (hHardy : PublishedHardyMultiplierEvaluation.{u})
    (B S : ℝ → H →L[ℂ] H)
    (hB : ∀ x, AEStronglyMeasurable (fun t => B t x) volume)
    (hS : ∀ x, AEStronglyMeasurable (fun t => S t x) volume)
    (CB CS : ℝ) (hb : ∀ᵐ t, ‖B t‖ ≤ CB) (hs : ∀ᵐ t, ‖S t‖ ≤ CS)
    (hBS : ∀ᵐ t, ‖B t * S t‖ ≤ CB * CS)
    (T V : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hBT : RepresentsOperatorField volume B T) (hSV : RepresentsOperatorField volume S V)
    (hT : PreservesProjectionNest regularFrequencyNest T)
    (hV : PreservesProjectionNest regularFrequencyNest V)
    (t r : ℝ) (hr : 0 < r) :
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.PreservesProjectionNest, OAI.KadisonKastler.regularFrequencyNest

theorem OAI.KadisonKastler.measurablePoissonAverage_sandwich_of_hardy line 85

Source documentation

The same identity with an arbitrary constant operator in the middle. Only the two boundary multipliers need to preserve the frequency nest.

theorem measurablePoissonAverage_sandwich_of_hardy
    (hHardy : PublishedHardyMultiplierEvaluation.{u})
    (B S : ℝ → H →L[ℂ] H)
    (hB : ∀ ξ, AEStronglyMeasurable (fun t => B t ξ) volume)
    (hS : ∀ ξ, AEStronglyMeasurable (fun t => S t ξ) volume)
    (CB CS : ℝ) (hb : ∀ᵐ t, ‖B t‖ ≤ CB) (hs : ∀ᵐ t, ‖S t‖ ≤ CS)
    (T V : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hBT : RepresentsOperatorField volume B T) (hSV : RepresentsOperatorField volume S V)
    (hT : PreservesProjectionNest regularFrequencyNest T)
    (hV : PreservesProjectionNest regularFrequencyNest V)
    (x : H →L[ℂ] H)
    (hBxS : ∀ ξ, AEStronglyMeasurable (fun t => (B t * x * S t) ξ) volume)
…

Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.RepresentsOperatorField, OAI.KadisonKastler.PreservesProjectionNest, OAI.KadisonKastler.regularFrequencyNest