OAI/Analysis/IrrationalRotation/Spectral/FieldResolvent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.WeightedShift.resolventCoefficient_bound line 14
  2. def OAI.Invariant233.WeightedShift.positiveResolventWeight line 19
  3. theorem OAI.Invariant233.WeightedShift.positiveResolventWeight_bound line 28
  4. theorem OAI.Invariant233.WeightedShift.positiveResolventWeight_measurable line 36
  5. def OAI.Invariant233.WeightedShift.positiveFieldResolvent line 42
  6. theorem OAI.Invariant233.WeightedShift.positiveFieldResolvent_ae line 49
  7. theorem OAI.Invariant233.WeightedShift.positiveFieldResolvent_nonneg line 57
  8. theorem OAI.Invariant233.WeightedShift.norm_positiveFieldResolvent_le line 68
  9. theorem OAI.Invariant233.WeightedShift.resolvent_scalar_identity line 74
  10. theorem OAI.Invariant233.WeightedShift.positiveFieldResolvent_mem_domain line 83
  11. theorem OAI.Invariant233.WeightedShift.fieldUnboundedMultiplier_positiveFieldResolvent line 98
  12. theorem OAI.Invariant233.WeightedShift.positiveFieldResolvent_apply_add_multiplier line 114
  13. theorem OAI.Invariant233.WeightedShift.fieldUnboundedMultiplier_domain_eq_resolvent_range line 138
  14. theorem OAI.Invariant233.WeightedShift.fieldUnboundedMultiplier_domain_invariant_of_commute_resolvent line 151
  15. theorem OAI.Invariant233.WeightedShift.fieldUnboundedMultiplier_commutes_of_commute_resolvent line 170