OAI/Probability/ParisiFinite/EmpiricalExpLog.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Empirical Exp Log.

  1. def OAI.SKCavity.empiricalExpLog line 64
  2. lemma OAI.SKCavity.empiricalExpLog_eq line 67
  3. lemma OAI.SKCavity.integrable_empiricalExpLog line 74
  4. lemma OAI.SKCavity.empiricalExpLog_error line 82
  5. lemma OAI.SKCavity.integral_empiricalExpLog_error line 106
  6. def OAI.SKCavity.clipField line 145
  7. lemma OAI.SKCavity.clipField_abs_le line 147
  8. lemma OAI.SKCavity.clipField_bounded line 153
  9. lemma OAI.SKCavity.continuous_clipField line 157
  10. lemma OAI.SKCavity.exp_clip_diff_sq_le line 161
  11. lemma OAI.SKCavity.exp_neg_clip_le line 172
  12. lemma OAI.SKCavity.integrable_clip_exp_diff_sq line 178
  13. lemma OAI.SKCavity.integrable_neg_clip_exp line 187
  14. lemma OAI.SKCavity.clipped_exp_L2_tendsto line 197
  15. lemma OAI.SKCavity.integrable_exp_abs_field line 215
  16. lemma OAI.SKCavity.integrable_exp_abs_lipschitz_field line 230
  17. lemma OAI.SKCavity.integrable_lipschitz_field line 244
  18. lemma OAI.SKCavity.scalarHierarchy_schedule line 263
  19. lemma OAI.SKCavity.gaussianHierarchy_cosh_schedule line 275
  20. lemma OAI.SKCavity.step_affine line 287
  21. lemma OAI.SKCavity.scalarHierarchy_affine line 303
  22. def OAI.SKCavity.hierarchyFieldValue line 324
  23. lemma OAI.SKCavity.hierarchyField_clip_error line 328
  24. theorem OAI.SKCavity.hierarchyField_lipschitz_tendsto line 387
  25. lemma OAI.SKCavity.initial_segment_square line 461
  26. def OAI.SKCavity.gridZVariance line 481
  27. def OAI.SKCavity.gridYVariance line 482
  28. lemma OAI.SKCavity.gridZVariance_nonneg line 484
  29. lemma OAI.SKCavity.gridYVariance_nonneg line 485
  30. lemma OAI.SKCavity.grid_tree_z_kernel line 487
  31. lemma OAI.SKCavity.grid_tree_y_kernel line 495
  32. lemma OAI.SKCavity.continuous_empiricalExpLog line 520
  33. lemma OAI.SKCavity.empiricalExpLog_cosh line 530
  34. lemma OAI.SKCavity.expected_empiricalExpLog line 537
  35. lemma OAI.SKCavity.coshGramPressure_field line 545
  36. lemma OAI.SKCavity.squareGramPressure_field line 572
  37. lemma OAI.SKCavity.hierarchyFieldValue_sum line 607
  38. lemma OAI.SKCavity.lipschitz_log_cosh line 628
  39. theorem OAI.SKCavity.gridCavityMixture_fields line 646