StrongCompressionBound.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering an operator norm bound from finite-corner bounds in a strongly exhausting family of compressions.

lemma OAI.WeakPureInfiniteness.strong_compressions_tendsto line 17

Source documentation

Uniformly contractive compressions converging strongly to the identity recover every operator strongly, including on its moving input vector.

lemma strong_compressions_tendsto (l : Filter ι) (P : ι → H →L[ℂ] H)
    (hPn : ∀ i, ‖P i‖ ≤ 1) (hP : ∀ x, Tendsto (fun i => P i x) l (𝓝 x))
    (T : H →L[ℂ] H) (x : H) :
    Tendsto (fun i => (P i * T * P i) x) l (𝓝 (T x)) := by
…

theorem OAI.WeakPureInfiniteness.norm_le_of_strong_compression_bound line 34

Source documentation

A bound on every strongly exhausting compression is a bound on the original operator. No norm convergence of the projections is needed.

theorem norm_le_of_strong_compression_bound (l : Filter ι) [NeBot l]
    (P : ι → H →L[ℂ] H) (hPn : ∀ i, ‖P i‖ ≤ 1)
    (hP : ∀ x, Tendsto (fun i => P i x) l (𝓝 x))
    (T : H →L[ℂ] H) {C : ℝ} (hC : 0 ≤ C)
    (hT : ∀ i, ‖P i * T * P i‖ ≤ C) : ‖T‖ ≤ C := by
…