OAI/Probability/ThreeStateClauses/PositiveMoments.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Positive Moments.

  1. def OAI.ThreeState.TreeClauses.Positive.fourthResolvent line 15
  2. def OAI.ThreeState.TreeClauses.Positive.fourthEdgeResolvent line 17
  3. def OAI.ThreeState.TreeClauses.Positive.momentA line 20
  4. def OAI.ThreeState.TreeClauses.Positive.momentQ line 22
  5. lemma OAI.ThreeState.TreeClauses.Positive.fourthMoment line 25
  6. lemma OAI.ThreeState.TreeClauses.Positive.fourthResolvent_eq line 29
  7. lemma OAI.ThreeState.TreeClauses.Positive.fraction_lower line 43
  8. lemma OAI.ThreeState.TreeClauses.Positive.fourthResolvent_nonneg line 71
  9. lemma OAI.ThreeState.TreeClauses.Positive.fourthResolvent_lower line 78
  10. lemma OAI.ThreeState.TreeClauses.Positive.fourthResolvent_continuousOn line 122
  11. lemma OAI.ThreeState.TreeClauses.Positive.lower_integral line 128
  12. theorem OAI.ThreeState.TreeClauses.Positive.momentA_lower line 137
  13. lemma OAI.ThreeState.TreeClauses.Positive.avg_mono line 150
  14. lemma OAI.ThreeState.TreeClauses.Positive.fourthResolvent_four line 154
  15. lemma OAI.ThreeState.TreeClauses.Positive.fourthEdgeResolvent_lower line 160
  16. lemma OAI.ThreeState.TreeClauses.Positive.fourthEdgeResolvent_continuousOn line 214
  17. theorem OAI.ThreeState.TreeClauses.Positive.momentQ_lower line 225
  18. def OAI.ThreeState.TreeClauses.Positive.residual line 254
  19. lemma OAI.ThreeState.TreeClauses.Positive.avg_integrable line 258
  20. lemma OAI.ThreeState.TreeClauses.Positive.avg_continuousOn line 262
  21. lemma OAI.ThreeState.TreeClauses.Positive.edge_message line 266
  22. lemma OAI.ThreeState.TreeClauses.Positive.centered_edge line 273
  23. lemma OAI.ThreeState.TreeClauses.Positive.symEntropy_integral line 276
  24. lemma OAI.ThreeState.TreeClauses.Positive.symEntropy_nonneg line 290
  25. lemma OAI.ThreeState.TreeClauses.Positive.residual_continuousOn line 298
  26. lemma OAI.ThreeState.TreeClauses.Positive.symEntropy_residual line 309
  27. lemma OAI.ThreeState.TreeClauses.Positive.powerResolvent_continuousOn line 345
  28. lemma OAI.ThreeState.TreeClauses.Positive.edge_symEntropy_integral line 355
  29. lemma OAI.ThreeState.TreeClauses.Positive.symEntropy_edge_residual line 367
  30. lemma OAI.ThreeState.TreeClauses.Positive.momentA_identity line 393
  31. lemma OAI.ThreeState.TreeClauses.Positive.momentY_residual line 419