OAI/NumberTheory/TwoPoint/Bounds/ResolventTransfer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The resolvent path for noncommuting edge operators

The definitions and lemmas here implement the path used in manuscript Lemma q:noncommuting. The only products that are commuted are an edge operator and its own resolvent.

  1. def OAI.TwoPointCorrelations.edgeResolvent line 25
  2. def OAI.TwoPointCorrelations.transferResolvent line 28
  3. def OAI.TwoPointCorrelations.nonbacktrackingContinuous line 31
  4. lemma OAI.TwoPointCorrelations.isUnit_edge_shift line 35
  5. lemma OAI.TwoPointCorrelations.edgeResolvent_mul line 41
  6. lemma OAI.TwoPointCorrelations.edgeResolvent_commute line 46
  7. lemma OAI.TwoPointCorrelations.transferResolvent_selfAdjoint line 62
  8. lemma OAI.TwoPointCorrelations.clm_injective_of_isUnit line 77
  9. theorem OAI.TwoPointCorrelations.transferResolvent_injective line 82
  10. theorem OAI.TwoPointCorrelations.transferResolvent_continuousOn line 101
  11. theorem OAI.TwoPointCorrelations.transferResolvent_positive line 120

    Source documentation

    The positivity step of the nonbacktracking spectral transfer.

    theorem transferResolvent_positive [Nontrivial E] (B : ι → E →L[ℂ] E)
    (hB : ∀ i, IsSelfAdjoint (B i)) (t : ℝ) (ht : 0 ≤ t)
    (hsmall : ∀ u ∈ Set.Icc 0 t, ∀ i, ‖u • B i‖ < 1)
    (hH : ∀ u ∈ Set.Icc 0 t,
      IsUnit (1 - (u : ℂ) • nonbacktrackingContinuous B)) :
    ∀ v : E, v ≠ 0 → 0 < (inner ℂ (transferResolvent B t v) v).re := by
…

    Mentions: OAI.TwoPointCorrelations.nonbacktrackingContinuous, OAI.TwoPointCorrelations.transferResolvent

  12. lemma OAI.TwoPointCorrelations.edgeResolvent_norm_le_two line 137
  13. lemma OAI.TwoPointCorrelations.nonbacktracking_resolvent_isUnit line 153