PoissonProductEstimates.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the two analytic smoothing fields

Boundary products of two approximate unitary fields have quadratic error. Once the Hardy product identity identifies their positive-height product with its Poisson integral, positivity of that integral retains the error. The product identity is a hypothesis of these estimates.

theorem OAI.KadisonKastler.norm_product_sub_product_of_contractions line 24

theorem OAI.KadisonKastler.operator_product_vector_measurable line 51

Source documentation

A product field is measurable on every vector, even when it is not measurable for the operator norm topology.

theorem operator_product_vector_measurable
    (B S : ℝ → H →L[ℂ] H)
    (hB : ∀ x, AEStronglyMeasurable (fun s => B s x) volume)
    (hS : ∀ x, AEStronglyMeasurable (fun s => S s x) volume) :
    ∀ x, AEStronglyMeasurable (fun s => (B s * S s) x) volume := by
…

theorem OAI.KadisonKastler.ae_product_error line 61

Source documentation

Uniform contraction targets give an essential product error.

theorem ae_product_error
    (B S U V : ℝ → H →L[ℂ] H) {δ : ℝ} (hδ : 0 ≤ δ)
    (hU : ∀ᵐ s, ‖U s‖ ≤ 1) (hV : ∀ᵐ s, ‖V s‖ ≤ 1)
    (hB : ∀ᵐ s, ‖B s - U s‖ ≤ δ) (hS : ∀ᵐ s, ‖S s - V s‖ ≤ δ) :
    ∀ᵐ s, ‖B s * S s - U s * V s‖ ≤ 2 * δ + δ ^ 2 := by
…

theorem OAI.KadisonKastler.norm_poisson_product_error line 70

Source documentation

Essential product bounds pass to every positive-height average.

theorem norm_poisson_product_error
    (B S U V : ℝ → H →L[ℂ] H)
    (hB : ∀ x, AEStronglyMeasurable (fun s => B s x) volume)
    (hS : ∀ x, AEStronglyMeasurable (fun s => S s x) volume)
    (hU : ∀ x, AEStronglyMeasurable (fun s => U s x) volume)
    (hV : ∀ x, AEStronglyMeasurable (fun s => V s x) volume)
    {CB CS : ℝ} (hb : ∀ᵐ s, ‖B s‖ ≤ CB) (hs : ∀ᵐ s, ‖S s‖ ≤ CS)
    (hCB : 0 ≤ CB)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hu : ∀ᵐ s, ‖U s‖ ≤ 1) (hv : ∀ᵐ s, ‖V s‖ ≤ 1)
    (hBU : ∀ᵐ s, ‖B s - U s‖ ≤ δ) (hSV : ∀ᵐ s, ‖S s - V s‖ ≤ δ)
    (t r : ℝ) (hr : 0 < r) :
…

theorem OAI.KadisonKastler.exp_mul_one_add_le line 99

Source documentation

The explicit demodulation factor grows at most linearly at small height.

theorem exp_mul_one_add_le {r δ : ℝ} (hr : 0 ≤ r) (hr1 : r ≤ 1)
    (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) :
    Real.exp r * (1 + δ) ≤ 1 + 4 * r + δ := by
…

theorem OAI.KadisonKastler.norm_demodulatedPoissonAverage_le_small line 113

Source documentation

The constructed Poisson smoothing has an absolute first-order norm bound.

theorem norm_demodulatedPoissonAverage_le_small
    (B : ℝ → H →L[ℂ] H)
    (hB : ∀ x, AEStronglyMeasurable (fun s => B s x) volume)
    {δ : ℝ} (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1)
    (hb : ∀ᵐ s, ‖B s‖ ≤ 1 + δ) (t r : ℝ) (hr : 0 < r) (hr1 : r ≤ 1) :
    ‖demodulatedPoissonAverage B hB (1 + δ) hb t r hr‖ ≤ 1 + 4 * r + δ :=
…

Mentions: OAI.KadisonKastler.demodulatedPoissonAverage