OAI/Probability/ThreeState/Resolvents.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Fourth-moment resolvents and their lower bounds.

  1. def OAI.ThreeState.Radial.fourthResolvent line 11
  2. def OAI.ThreeState.Radial.doubleFourthResolvent line 12
  3. lemma OAI.ThreeState.Radial.fourth_moment line 15
  4. lemma OAI.ThreeState.Radial.fourthResolvent_eq line 19
  5. lemma OAI.ThreeState.Radial.h_polynomial_bound line 34
  6. lemma OAI.ThreeState.Radial.momentY_sqrt_bound line 45
  7. lemma OAI.ThreeState.Radial.fourthResolvent_lower line 57
  8. lemma OAI.ThreeState.Radial.fourthResolvent_four line 91
  9. lemma OAI.ThreeState.Radial.doubleFourthResolvent_lower line 100
  10. lemma OAI.ThreeState.Radial.continuousOn_fourthResolvent line 140
  11. lemma OAI.ThreeState.Radial.continuousOn_doubleFourthResolvent line 148
  12. def OAI.ThreeState.Radial.resolventA line 159
  13. def OAI.ThreeState.Radial.resolventQ line 160
  14. def OAI.ThreeState.Radial.functionJ line 161
  15. lemma OAI.ThreeState.Radial.integral_h_lower line 163
  16. lemma OAI.ThreeState.Radial.resolventA_lower line 176
  17. lemma OAI.ThreeState.Radial.resolventQ_lower line 189
  18. lemma OAI.ThreeState.Radial.scalar_resolventA line 203
  19. lemma OAI.ThreeState.Radial.resolventA_identity line 226
  20. lemma OAI.ThreeState.Radial.resolvent_scaling line 240
  21. lemma OAI.ThreeState.Radial.momentX_scale line 270
  22. lemma OAI.ThreeState.Radial.momentY_scale line 273
  23. lemma OAI.ThreeState.Radial.resolventQ_identity line 276