SpectralTransfer.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Noncommuting spectral transfer

The manuscript's Lemma q:noncommuting, in a form with any common upper bound on the single-edge norms, the square function, and the spectral radius. No commutation between distinct edges is assumed.

lemma OAI.TwoPointCorrelations.projection_norm_apply_le line 20
lemma OAI.TwoPointCorrelations.compression_norm_le_of_quadratic line 39

theorem OAI.TwoPointCorrelations.noncommuting_spectral_transfer line 68

Source documentation

A common-bound version of the noncommuting transfer lemma.

theorem noncommuting_spectral_transfer
    (B : ι → E →L[ℂ] E) (hB : ∀ i, IsSelfAdjoint (B i))
    (P : E →L[ℂ] E) (hP : IsSelfAdjoint P) (hPP : P * P = P)
    (m : ℝ≥0) (hnorm : ∀ i, ‖B i‖ ≤ (m : ℝ))
    (hsq : ∀ v : E, P v = v → ∑ i, ‖B i v‖ ^ 2 ≤ (m : ℝ) ^ 2 * ‖v‖ ^ 2)
    (hrad : spectralRadius ℂ (nonbacktrackingContinuous B) ≤ (m : ℝ≥0∞)) :
    ‖P * (∑ i, B i) * P‖ ≤ 3 * (m : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.nonbacktrackingContinuous

theorem OAI.TwoPointCorrelations.noncommuting_spectral_transfer_max line 117

Source documentation

Lemma q:noncommuting, with its three separate bounds. The spectral radius is finite because the operator is bounded.

theorem noncommuting_spectral_transfer_max
    (B : ι → E →L[ℂ] E) (hB : ∀ i, IsSelfAdjoint (B i))
    (P : E →L[ℂ] E) (hP : IsSelfAdjoint P) (hPP : P * P = P)
    (a b : ℝ≥0) (hnorm : ∀ i, ‖B i‖ ≤ (a : ℝ))
    (hsq : ∀ v : E, P v = v → ∑ i, ‖B i v‖ ^ 2 ≤ (b : ℝ) ^ 2 * ‖v‖ ^ 2) :
    ‖P * (∑ i, B i) * P‖ ≤
      3 * ((max (max a b) ((spectralRadius ℂ (nonbacktrackingContinuous B)).toNNReal) : ℝ≥0) : ℝ) := by
…

Mentions: OAI.TwoPointCorrelations.nonbacktrackingContinuous