OAI/Analysis/KadisonKastler/DemodulatedInverseBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Approximate inverses after Poisson demodulation

The Hardy product identity follows from the published evaluation input on the concrete positive-frequency algebra. The scalar Poisson character formula is proved, and inverse estimates use the actual boundary product.

  1. theorem OAI.KadisonKastler.norm_demodulatedPoisson_product_sub_one_le_of_product_identity line 24
  2. theorem OAI.KadisonKastler.norm_demodulatedPoisson_product_sub_one_le line 78
  3. theorem OAI.KadisonKastler.exp_two_mul_product_error_le line 114

    Source documentation

    A small boundary error and a no-larger positive height give a linear inverse error with an absolute constant.

    theorem exp_two_mul_product_error_le {r δ : ℝ}
    (hr : 0 ≤ r) (hrδ : r ≤ δ) (hδ : 0 ≤ δ) (hδsmall : δ ≤ 1 / 8) :
    Real.exp (2 * r) * (2 * δ + δ ^ 2) ≤ 6 * δ := by
…