UltrapowerSpectralCompression.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative finite spectral abelianization in a norm ultrapower. The coefficient bound is chosen before the mesh, as required for taking the mesh to zero. The resulting compressor is an element of the original ultrapower.

theorem OAI.WeakPureInfiniteness.ultrapower_spectral_compression_bounds line 24

Source documentation

The two-pass Gram construction and the joint spectral partition give one contractive compression, preserving the first two moments and making its image of one coefficient approximately commute with the selected elements.

theorem ultrapower_spectral_compression_bounds (hP : MainGap.PropertyP A)
    (a : I → N) (ha : ∀ i, 0 ≤ a i) (hc : ∀ i j, Commute (a i) (a j))
    (b : N) (hb : IsSelfAdjoint b) (δ η : ℝ≥0) (hδ : 0 < δ) (hη : 0 < η)
    (hcut : (δ + η : ℝ≥0) < 1) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ r : ℝ, 0 < r → r ≤ 1 →
      ∃ v : N, ‖v‖ ≤ 1 ∧ ∀ i,
        ‖star v * a i * v - a i‖ ≤
          (2 * r * Real.sqrt ((5 : ℝ) ^ Fintype.card I)) * C +
            (r + (δ + η : ℝ≥0) * (‖a i‖ + r)) ∧
        ‖star v * (a i * a i) * v - a i * a i‖ ≤
          (‖a i‖ + ((∑ k, ‖a k‖) + 2)) *
            ((2 * r * Real.sqrt ((5 : ℝ) ^ Fintype.card I)) * C) +
…

Mentions: OAI.MainGap.PropertyP