SupportBounds.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Square sums over orthogonal supports

These are the Hilbert-space estimates converting bounds through each diagonal label into the uniform coefficient-column drift in §3.

theorem OAI.KadisonKastler.norm_sum_sq_of_pairwise_orthogonal line 20

theorem OAI.KadisonKastler.weighted_orthogonal_supports_le line 39

Source documentation

A bound on the squared weights through each label controls the sum over all supports. Each support is counted just once.

theorem weighted_orthogonal_supports_le {ι ω : Type*} [Fintype ι] [DecidableEq ι] [Fintype ω]
    (v : ι → H) (S : ω → Finset ι) (β : ω → ℝ) {B : ℝ}
    (hv : Pairwise (fun i j => inner ℂ (v i) (v j) = 0))
    (hβ : ∀ i, (∑ w : ω, if i ∈ S w then β w ^ 2 else 0) ≤ B) :
    (∑ w : ω, β w ^ 2 * ‖∑ i ∈ S w, v i‖ ^ 2) ≤
      B * ‖∑ i : ι, v i‖ ^ 2 := by
…

theorem OAI.KadisonKastler.orthogonal_projection_vectors line 67

theorem OAI.KadisonKastler.weighted_projection_supports_le line 82

Source documentation

The support-weighted estimate for an actual orthogonal partition of the identity in an operator algebra.

theorem weighted_projection_supports_le {ι ω : Type*} [Fintype ι] [DecidableEq ι] [Fintype ω]
    (P : ι → H →L[ℂ] H) (S : ω → Finset ι) (β : ω → ℝ) {B : ℝ}
    (hself : ∀ i, IsSelfAdjoint (P i))
    (horth : ∀ i j, i ≠ j → P i * P j = 0) (htotal : ∑ i, P i = 1)
    (hβ : ∀ i, (∑ w : ω, if i ∈ S w then β w ^ 2 else 0) ≤ B) (x : H) :
    (∑ w : ω, β w ^ 2 * ‖(∑ i ∈ S w, P i) x‖ ^ 2) ≤ B * ‖x‖ ^ 2 := by
…

theorem OAI.KadisonKastler.support_drift_le_sixty_four line 94

Source documentation

The through-label square bound 64, together with the cyclic column constant 8, gives the coefficient drift constant 64.

theorem support_drift_le_sixty_four {ι ω : Type*} [Fintype ι] [DecidableEq ι] [Fintype ω]
    (P : ι → H →L[ℂ] H) (S : ω → Finset ι) (β : ω → ℝ)
    (hself : ∀ i, IsSelfAdjoint (P i))
    (horth : ∀ i j, i ≠ j → P i * P j = 0) (htotal : ∑ i, P i = 1)
    (hβ : ∀ i, (∑ w : ω, if i ∈ S w then β w ^ 2 else 0) ≤ 64)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (D : ω → H) (x : H)
    (hD : ∀ w, ‖D w‖ ≤ 8 * δ * β w * ‖(∑ i ∈ S w, P i) x‖) :
    ‖WithLp.toLp 2 D‖ ≤ 64 * δ * ‖x‖ := by
…

theorem OAI.KadisonKastler.norm_pointwise_operator_le line 124

Source documentation

Applying one bounded operator in every component has the same bound on the Hilbert direct sum.

theorem norm_pointwise_operator_le {ω : Type*} [Fintype ω]
    (T : H →L[ℂ] H) (v : ω → H) :
    ‖WithLp.toLp 2 (fun w => T (v w))‖ ≤ ‖T‖ * ‖WithLp.toLp 2 v‖ := by
…

theorem OAI.KadisonKastler.norm_column_commutator_le line 136

Source documentation

A contractive column of coefficients costs at most twice the norm of a perturbation when commuting that perturbation past the column.

theorem norm_column_commutator_le {ω : Type*} [Fintype ω]
    (K : ω → H →L[ℂ] H)
    (hK : ∀ y : H, ‖WithLp.toLp 2 (fun w => K w y)‖ ≤ ‖y‖)
    (T : H →L[ℂ] H) (x : H) :
    ‖WithLp.toLp 2 (fun w => (T * K w - K w * T) x)‖ ≤ 2 * ‖T‖ * ‖x‖ := by
…

theorem OAI.KadisonKastler.coefficient_drift_le_sixty_six line 156

Source documentation

The 64δ bound obtained after averaging changes to 66δ for the original implementing operator.

theorem coefficient_drift_le_sixty_six {ω : Type*} [Fintype ω]
    (K : ω → H →L[ℂ] H)
    (hK : ∀ y : H, ‖WithLp.toLp 2 (fun w => K w y)‖ ≤ ‖y‖)
    (h h0 : H →L[ℂ] H) {δ : ℝ} (hclose : ‖h - h0‖ ≤ δ)
    (x : H)
    (hbound : ‖WithLp.toLp 2 (fun w => (h0 * K w - K w * h0) x)‖ ≤
      64 * δ * ‖x‖) :
    ‖WithLp.toLp 2 (fun w => (h * K w - K w * h) x)‖ ≤ 66 * δ * ‖x‖ := by
…