PoissonBoundaryLimit.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The strong-star boundary comparison used in modular smoothing

The demodulated Cauchy averages are actual bounded operators. Their products converge strongly-* even though the polar smoothing paths need not converge.

theorem OAI.KadisonKastler.norm_unitary_le_one' line 22
def OAI.KadisonKastler.modulatedUnitaryField line 27
theorem OAI.KadisonKastler.modulatedUnitaryField_continuous line 30
theorem OAI.KadisonKastler.modulatedUnitaryField_star_continuous line 35
theorem OAI.KadisonKastler.norm_modulatedUnitaryField_le_one line 46

def OAI.KadisonKastler.poissonBoundaryApprox line 52

Source documentation

The scalar factor is exp(-i(t+ir)) = exp(r) exp(-it).

def poissonBoundaryApprox (W : ℝ → unitary (H →L[ℂ] H))
    (hW : ∀ x, Continuous (fun t => (W t : H →L[ℂ] H) x)) (t r : ℝ) : H →L[ℂ] H :=
…

theorem OAI.KadisonKastler.norm_poissonBoundaryApprox_le line 58
theorem OAI.KadisonKastler.poissonBoundaryApprox_tendsto line 72
theorem OAI.KadisonKastler.poissonBoundaryApprox_star_tendsto line 89

theorem OAI.KadisonKastler.tendsto_operator_comp_of_uniform_bound line 111

Source documentation

Multiplication is strongly continuous on a family with bounded left operator norms; the right arguments may also vary.

theorem tendsto_operator_comp_of_uniform_bound {ι : Type*} {l : Filter ι}
    (A B : ι → H →L[ℂ] H) (T S : H →L[ℂ] H) (C : ℝ)
    (hbound : ∀ᶠ i in l, ‖A i‖ ≤ C)
    (hA : ∀ x, Tendsto (fun i => A i x) l (𝓝 (T x)))
    (hB : ∀ x, Tendsto (fun i => B i x) l (𝓝 (S x))) (x : H) :
    Tendsto (fun i => (A i * B i) x) l (𝓝 ((T * S) x)) := by
…

def OAI.KadisonKastler.poissonBoundaryQuotient line 136
theorem OAI.KadisonKastler.norm_poissonBoundaryQuotient_le line 140

theorem OAI.KadisonKastler.poissonBoundaryQuotient_tendsto line 150

Source documentation

The product comparison used in the UCP limit converges strongly-* at all fixed times.

theorem poissonBoundaryQuotient_tendsto (W : ℝ → unitary (H →L[ℂ] H))
    (hW : ∀ x, Continuous (fun t => (W t : H →L[ℂ] H) x))
    (hWs : ∀ x, Continuous (fun t => star (W t : H →L[ℂ] H) x))
    (hzero : W 0 = 1) (t : ℝ) (x : H) :
    Tendsto (fun r => poissonBoundaryQuotient W hW t r x) (𝓝 0)
      (𝓝 ((W t : H →L[ℂ] H) x)) ∧
    Tendsto (fun r => star (poissonBoundaryQuotient W hW t r) x) (𝓝 0)
      (𝓝 (star (W t : H →L[ℂ] H) x)) := by
…

Mentions: OAI.KadisonKastler.poissonBoundaryQuotient