OAI/Probability/ParisiFinite/OrderPointIntegrable.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Order Point Integrable.

  1. lemma OAI.ParisiFinite.orderPoint_integrable line 64
  2. lemma OAI.ParisiFinite.orderPoint_mean_zero_iff line 69
  3. lemma OAI.ParisiFinite.minimizingParisi_mean_pos line 93
  4. lemma OAI.ParisiFinite.hasDerivAt_tiltedMean line 116
  5. structure OAI.ParisiFinite.ThirdJet line 139
  6. def OAI.ParisiFinite.ThirdJet.expThird line 149
  7. lemma OAI.ParisiFinite.ThirdJet.continuous_expThird line 152
  8. lemma OAI.ParisiFinite.ThirdJet.product_bound line 159
  9. lemma OAI.ParisiFinite.ThirdJet.cube_bound line 163
  10. lemma OAI.ParisiFinite.ThirdJet.expThird_bound line 167
  11. def OAI.ParisiFinite.ThirdJet.transformD3 line 177
  12. lemma OAI.ParisiFinite.ThirdJet.expThird_tilt line 182
  13. lemma OAI.ParisiFinite.ThirdJet.hasDerivAt_transformD2 line 205
  14. lemma OAI.ParisiFinite.ThirdJet.continuous_transformD3 line 231
  15. lemma OAI.ParisiFinite.ThirdJet.transformD3_bound line 243
  16. def OAI.ParisiFinite.ThirdJet.transform line 259
  17. lemma OAI.ParisiFinite.ThirdJet.expThird_transform line 269