OAI/Probability/ThreeStateClauses/RadialCalculus.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Radial Calculus.

  1. def OAI.ThreeState.TreeClauses.Radial.rayG₀ line 14
  2. def OAI.ThreeState.TreeClauses.Radial.rayG₁ line 15
  3. def OAI.ThreeState.TreeClauses.Radial.rayG₂ line 16
  4. def OAI.ThreeState.TreeClauses.Radial.rayG₃ line 17
  5. def OAI.ThreeState.TreeClauses.Radial.rayI₀ line 19
  6. def OAI.ThreeState.TreeClauses.Radial.rayI₁ line 20
  7. def OAI.ThreeState.TreeClauses.Radial.rayI₂ line 21
  8. def OAI.ThreeState.TreeClauses.Radial.rayI₃ line 22
  9. def OAI.ThreeState.TreeClauses.Radial.rayH₀ line 24
  10. def OAI.ThreeState.TreeClauses.Radial.rayH₁ line 25
  11. def OAI.ThreeState.TreeClauses.Radial.rayH₂ line 26
  12. def OAI.ThreeState.TreeClauses.Radial.rayH₃ line 27
  13. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_avg line 29
  14. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_ray_coord line 34
  15. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayG₀ line 38
  16. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayG₁ line 42
  17. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayG₂ line 49
  18. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayI₀ line 57
  19. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayI₁ line 67
  20. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayI₂ line 74
  21. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayH₀ line 81
  22. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayH₁ line 92
  23. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayH₂ line 100
  24. def OAI.ThreeState.TreeClauses.Radial.rayF₀ line 110
  25. def OAI.ThreeState.TreeClauses.Radial.rayF₁ line 113
  26. def OAI.ThreeState.TreeClauses.Radial.rayF₂ line 117
  27. def OAI.ThreeState.TreeClauses.Radial.rayF₃ line 122
  28. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayF₀ line 128
  29. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayF₁ line 139
  30. lemma OAI.ThreeState.TreeClauses.Radial.hasDerivAt_rayF₂ line 152
  31. lemma OAI.ThreeState.TreeClauses.Radial.rayF₀_eq_functional line 168
  32. lemma OAI.ThreeState.TreeClauses.Radial.rayF₀_zero line 175
  33. lemma OAI.ThreeState.TreeClauses.Radial.rayF₁_zero line 178
  34. lemma OAI.ThreeState.TreeClauses.Radial.rayG₁_scaled line 181
  35. lemma OAI.ThreeState.TreeClauses.Radial.rayG₂_scaled line 189
  36. lemma OAI.ThreeState.TreeClauses.Radial.rayG₃_scaled line 197
  37. lemma OAI.ThreeState.TreeClauses.Radial.rayI₁_scaled line 207
  38. lemma OAI.ThreeState.TreeClauses.Radial.rayI₂_scaled line 210
  39. lemma OAI.ThreeState.TreeClauses.Radial.rayI₃_scaled line 219
  40. lemma OAI.ThreeState.TreeClauses.Radial.rayH₃_scaled line 229
  41. lemma OAI.ThreeState.TreeClauses.Radial.logMoment_ray line 242
  42. lemma OAI.ThreeState.TreeClauses.Radial.rayF₃_scaled line 247
  43. lemma OAI.ThreeState.TreeClauses.Radial.monotoneOn_Icc_of_hasDerivAt_nonneg line 269
  44. lemma OAI.ThreeState.TreeClauses.Radial.radial_calculus line 279
  45. lemma OAI.ThreeState.TreeClauses.Radial.positive_edge line 336
  46. lemma OAI.ThreeState.TreeClauses.Radial.momentX_edge line 343
  47. lemma OAI.ThreeState.TreeClauses.Radial.rayF₃_lower line 347
  48. theorem OAI.ThreeState.TreeClauses.Radial.radial_inequality line 359