SourceIncrementalPatching.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Incremental moment patches chosen inside a prescribed irreducible source.

theorem OAI.KadisonSimilarity.exists_source_incremental_patch line 27

Source documentation

The mixed-word patch is an extension in the source algebra, even though all coefficients and estimates belong to the larger ambient algebra.

theorem exists_source_incremental_patch {I : Type*} [Fintype I]
    (F : I → M.toStarSubalgebra)
    (hF : ∀ i, ‖F i‖ ≤ 1) (hFτ : ∀ i, υ.trace (F i) = 0)
    {K N : ℕ} (hK : 0 < K) {b : ℝ → ℝ} (v : PartialUnitary R.toStarSubalgebra)
    (hb : 0 ≤ b ((υ.trace (coordinateInclusion hRM v.support)).re))
    (hv : MomentBound F (vectorPositiveFunctional M υ.vector) (K := K) (N := N) b
…

Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional