OAI/Analysis/BackwardIntertwiners/WeightSeparation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BackwardIntertwiners.QuadraticWeights line 11
  2. def OAI.BackwardIntertwiners.SupportSeparation line 22
  3. def OAI.BackwardIntertwiners.reflectedWeight line 30
  4. lemma OAI.BackwardIntertwiners.reflectedWeight_pos line 32
  5. lemma OAI.BackwardIntertwiners.reflectedWeight_antitone line 35
  6. lemma OAI.BackwardIntertwiners.reflected_positiveLog line 40
  7. lemma OAI.BackwardIntertwiners.reflected_negativeLog line 44
  8. lemma OAI.BackwardIntertwiners.reflected_stepRatio_summable line 48
  9. lemma OAI.BackwardIntertwiners.reflected_correlations line 59
  10. lemma OAI.BackwardIntertwiners.reflected_bounds line 75
  11. theorem OAI.BackwardIntertwiners.normalized_support_separation line 89
  12. lemma OAI.BackwardIntertwiners.DiscreteConvex.add_const line 169
  13. lemma OAI.BackwardIntertwiners.eventually_quadratic_lower line 174
  14. theorem OAI.BackwardIntertwiners.quadratic_support_separation line 184
  15. lemma OAI.BackwardIntertwiners.SupportSeparation.of_bounded line 260