AnalyticAlgebraBounds.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Algebra errors of the demodulated analytic products

The Hardy product identity follows from evaluation and preservation of the frequency nest. The resulting norm estimates pass from boundary algebra distance to positive-height distance.

theorem OAI.KadisonKastler.norm_sandwich_sub_of_contractions line 31

Source documentation

Perturbing both factors gives the boundary sandwich error.

theorem norm_sandwich_sub_of_contractions
    (a b u v x : H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hu : ‖u‖ ≤ 1) (hv : ‖v‖ ≤ 1)
    (ha : ‖a - u‖ ≤ δ) (hb : ‖b - v‖ ≤ δ) :
    ‖a * x * b - u * x * v‖ ≤ (2 * δ + δ ^ 2) * ‖x‖ := by
…

theorem OAI.KadisonKastler.sandwich_vector_measurable line 56
theorem OAI.KadisonKastler.ae_norm_sandwich_le line 66

theorem OAI.KadisonKastler.infDist_poisson_sandwich_le line 78

Source documentation

The actual Poisson average of a product inherits its boundary algebra error. This is the step for which no measurable nearest points are chosen.

theorem infDist_poisson_sandwich_le
    (M : VonNeumannAlgebra H)
    (hDistance : PublishedBlockCommutantApproximation (Algebra M.commutant) H)
    (B S U V : ℝ → H →L[ℂ] H)
    (hB : ∀ ξ, AEStronglyMeasurable (fun s => B s ξ) volume)
    (hS : ∀ ξ, AEStronglyMeasurable (fun s => S s ξ) volume)
    {CB CS : ℝ} (hCB : 0 ≤ CB)
    (hb : ∀ᵐ s, ‖B s‖ ≤ CB) (hs : ∀ᵐ s, ‖S s‖ ≤ CS)
    {δ e : ℝ} (hδ : 0 ≤ δ) (he : 0 ≤ e)
    (hu : ∀ᵐ s, ‖U s‖ ≤ 1) (hv : ∀ᵐ s, ‖V s‖ ≤ 1)
    (hBU : ∀ᵐ s, ‖B s - U s‖ ≤ δ) (hSV : ∀ᵐ s, ‖S s - V s‖ ≤ δ)
    (x : H →L[ℂ] H)
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.infDist_demodulated_sandwich_le_of_product_identity line 107

Source documentation

The published Hardy evaluation and actual frequency preservation give the quantitative demodulated algebra error at every positive height.

private theorem infDist_demodulated_sandwich_le_of_product_identity
    (M : VonNeumannAlgebra H)
    (hDistance : PublishedBlockCommutantApproximation (Algebra M.commutant) H)
    (B S U V : ℝ → H →L[ℂ] H)
    (hB : ∀ ξ, AEStronglyMeasurable (fun s => B s ξ) volume)
    (hS : ∀ ξ, AEStronglyMeasurable (fun s => S s ξ) volume)
    {CB CS : ℝ} (hCB : 0 ≤ CB)
    (hb : ∀ᵐ s, ‖B s‖ ≤ CB) (hs : ∀ᵐ s, ‖S s‖ ≤ CS)
    {δ e : ℝ} (hδ : 0 ≤ δ) (he : 0 ≤ e)
    (hu : ∀ᵐ s, ‖U s‖ ≤ 1) (hv : ∀ᵐ s, ‖V s‖ ≤ 1)
    (hBU : ∀ᵐ s, ‖B s - U s‖ ≤ δ) (hSV : ∀ᵐ s, ‖S s - V s‖ ≤ δ)
    (x : H →L[ℂ] H)
…

Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.infDist_demodulated_sandwich_le line 148