ResolventBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Quadratic-form bounds for the noncommuting resolvent

The correction is estimated using the norm of each individual resolvent. This avoids imposing any commutation relation between distinct edges.

theorem OAI.TwoPointCorrelations.transferResolvent_positive_abs line 19
theorem OAI.TwoPointCorrelations.transferResolvent_apply_expansion line 43
theorem OAI.TwoPointCorrelations.resolventCorrection_bound line 61
theorem OAI.TwoPointCorrelations.transferResolvent_inner_expansion line 96

theorem OAI.TwoPointCorrelations.edge_sum_quadratic_bound line 109

Source documentation

Positivity of the resolvent at both endpoints controls the quadratic form of the edge sum on each vector satisfying the square-function bound.

theorem edge_sum_quadratic_bound [Nontrivial E] (B : ι → E →L[ℂ] E)
    (hB : ∀ i, IsSelfAdjoint (B i)) (t b : ℝ) (ht : 0 < t)
    (hsmall : ∀ i, ‖t • B i‖ ≤ 1 / 2)
    (hplus : ∀ v : E, 0 ≤ (inner ℂ (transferResolvent B t v) v).re)
    (hminus : ∀ v : E, 0 ≤ (inner ℂ (transferResolvent B (-t) v) v).re)
    (v : E) (hsq : ∑ i, ‖B i v‖ ^ 2 ≤ b ^ 2 * ‖v‖ ^ 2) :
    |(inner ℂ (∑ i, B i v) v).re| ≤ ((1 + 2 * t ^ 2 * b ^ 2) / t) * ‖v‖ ^ 2 := by
…

Mentions: OAI.TwoPointCorrelations.transferResolvent