QuadraticBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Extracting a commutator bound from quadratic forms

This is the final operator-norm step of the randomized amplification argument in §3. The scalar recovery estimate is kept explicit.

theorem OAI.KadisonKastler.norm_le_of_selfAdjoint_quadratic line 19

theorem OAI.KadisonKastler.norm_le_of_unit_selfAdjoint_quadratic line 34

Source documentation

A unit-sphere quadratic estimate suffices for the full operator norm.

theorem norm_le_of_unit_selfAdjoint_quadratic (T : H →L[ℂ] H) (hT : IsSelfAdjoint T)
    {C : ℝ} (hC : 0 ≤ C)
    (hquad : ∀ x : H, ‖x‖ = 1 → |(inner ℂ (T x) x).re| ≤ C) :
    ‖T‖ ≤ C := by
…

theorem OAI.KadisonKastler.norm_commutator_le_of_quadratic line 60

Source documentation

A bound on the difference of a selfadjoint quadratic form before and after a unitary gives the same bound on its commutator with the unitary.

theorem norm_commutator_le_of_quadratic (h : H →L[ℂ] H) (hh : IsSelfAdjoint h)
    (u : unitary (H →L[ℂ] H)) {C : ℝ} (hC : 0 ≤ C)
    (hquad : ∀ x : H,
      |(inner ℂ (h x) x).re - (inner ℂ (h ((u : H →L[ℂ] H) x))
          ((u : H →L[ℂ] H) x)).re| ≤ C * ‖x‖ ^ 2) :
    ‖h * (u : H →L[ℂ] H) - (u : H →L[ℂ] H) * h‖ ≤ C := by
…

theorem OAI.KadisonKastler.norm_commutator_le_of_unit_quadratic line 90

Source documentation

The unit-sphere version used after the randomized-row estimate.

theorem norm_commutator_le_of_unit_quadratic (h : H →L[ℂ] H) (hh : IsSelfAdjoint h)
    (u : unitary (H →L[ℂ] H)) {C : ℝ} (hC : 0 ≤ C)
    (hquad : ∀ x : H, ‖x‖ = 1 →
      |(inner ℂ (h x) x).re - (inner ℂ (h ((u : H →L[ℂ] H) x))
        ((u : H →L[ℂ] H) x)).re| ≤ C) :
    ‖h * (u : H →L[ℂ] H) - (u : H →L[ℂ] H) * h‖ ≤ C := by
…

theorem OAI.KadisonKastler.norm_commutator_le_two_eighty_two line 120

Source documentation

The scalar lower bound 1/2 in the recovery argument converts its 141δ quadratic estimate into the 282δ unitary commutator estimate.

theorem norm_commutator_le_two_eighty_two (h : H →L[ℂ] H) (hh : IsSelfAdjoint h)
    (u : unitary (H →L[ℂ] H)) {δ : ℝ} (hδ : 0 ≤ δ)
    (hquad : ∀ x : H, ∃ c : ℝ, 1 / 2 ≤ c ∧
      c * |(inner ℂ (h x) x).re - (inner ℂ (h ((u : H →L[ℂ] H) x))
        ((u : H →L[ℂ] H) x)).re| ≤ 141 * δ * ‖x‖ ^ 2) :
    ‖h * (u : H →L[ℂ] H) - (u : H →L[ℂ] H) * h‖ ≤ 282 * δ := by
…