NormAttainingGrothendieck.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The norm-attaining case of the little Grothendieck inequality. The unitary paths and their quadratic estimates are constructed explicitly.

theorem OAI.KadisonSimilarity.exists_normAttainingState line 18

Source documentation

At a norm-attaining unit, the supporting vector functional is a state.

theorem exists_normAttainingState (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (h1 : ‖T 1‖ = 1) :
    ∃ f : A →ₚ[ℂ] ℂ, f 1 = 1 ∧ ∀ a, f a = inner ℂ (T 1) (T a) := by
…

theorem OAI.KadisonSimilarity.contraction_sqrt_complement line 41

Source documentation

The two conjugate unitary paths give a quadratic contraction estimate.

theorem contraction_sqrt_complement (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (a : A) (ha : IsSelfAdjoint a) (hna : ‖a‖ ≤ 1) :
    ‖T a‖ ^ 2 + ‖T (CFC.sqrt (1 - a ^ 2))‖ ^ 2 ≤ 1 := by
…

theorem OAI.KadisonSimilarity.sqrt_complement_remainder line 69
Source documentation
A scalar square-root expansion with a uniform quadratic remainder.
```
theorem sqrt_complement_remainder (s : ℝ) (hs0 : 0 ≤ s) (hs1 : s ≤ 1 / 2) :
    |1 - Real.sqrt (1 - s) - s / 2| ≤ s ^ 2 := by
…
```
def OAI.KadisonSimilarity.cfcSqrtRemainder line 85
Source documentation
The fourth-order remainder for the unitary path, still expressed in one continuous functional calculus.
```
def cfcSqrtRemainder (a : A) (t : ℝ) : A :=
…
```
theorem OAI.KadisonSimilarity.norm_cfcSqrtRemainder_le line 89

theorem OAI.KadisonSimilarity.cfcSqrtRemainder_eq line 106

Source documentation

Interpret the scalar remainder as the actual square-root error.

theorem cfcSqrtRemainder_eq (a : A) (ha : IsSelfAdjoint a) (t : ℝ)
    (hpos : 0 ≤ 1 - (t • a) ^ 2) :
    cfcSqrtRemainder a t =
      1 - CFC.sqrt (1 - (t • a) ^ 2) - (t ^ 2 / 2) • a ^ 2 := by
…

Mentions: OAI.KadisonSimilarity.cfcSqrtRemainder

theorem OAI.KadisonSimilarity.le_of_scaled_quadratic_approximations line 131

Source documentation

A fourth-order error disappears after dividing the quadratic term.

theorem le_of_scaled_quadratic_approximations {x y : ℝ}
    (h : ∀ t : ℝ, 0 < t → t ≤ 1 / 2 → t ^ 2 * x ≤ t ^ 2 * y + 2 * t ^ 4) :
    x ≤ y := by
…

theorem OAI.KadisonSimilarity.normAttaining_selfAdjoint_contraction line 150

Source documentation

The unitary-path estimate recovers the square bound on self-adjoint contractions.

theorem normAttaining_selfAdjoint_contraction (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (h1 : ‖T 1‖ = 1) (a : A) (ha : IsSelfAdjoint a) (hna : ‖a‖ ≤ 1) :
    ‖T a‖ ^ 2 ≤ (inner ℂ (T 1) (T (a ^ 2))).re := by
…

theorem OAI.KadisonSimilarity.normAttaining_selfAdjoint line 189

Source documentation

Homogeneity removes the contraction restriction.

theorem normAttaining_selfAdjoint (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (h1 : ‖T 1‖ = 1) (a : A) (ha : IsSelfAdjoint a) :
    ‖T a‖ ^ 2 ≤ (inner ℂ (T 1) (T (a ^ 2))).re := by
…

theorem OAI.KadisonSimilarity.normAttaining_grothendieck line 208

Source documentation

Haagerup's norm-attaining inequality, obtained from the real and imaginary parts.

theorem normAttaining_grothendieck (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (h1 : ‖T 1‖ = 1) :
    ∃ f : A →ₚ[ℂ] ℂ, f 1 = 1 ∧
      ∀ a, ‖T a‖ ^ 2 ≤ (f (star a * a)).re + (f (a * star a)).re := by
…

theorem OAI.KadisonSimilarity.unitaryNormAttaining_grothendieck line 232

Source documentation

Transport the norm-attaining inequality from the identity to a unitary.

theorem unitaryNormAttaining_grothendieck (T : A →L[ℂ] H) (hT : ‖T‖ ≤ 1)
    (u : unitary A) (hu : ‖T (u : A)‖ = 1) :
    ∃ f g : A →ₚ[ℂ] ℂ, f 1 = 1 ∧ g 1 = 1 ∧
      ∀ a, ‖T a‖ ^ 2 ≤ (f (star a * a)).re + (g (a * star a)).re := by
…