OAI/Probability/FreeIsing/Estimates/BoundedInnovationDrift.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.intervalIntegrable_of_measurable_norm_le_const line 12
  2. theorem OAI.Problem367.lipschitzWith_intervalPrimitive_of_bound line 19
  3. theorem OAI.Problem367.intervalIntegrable_nnreal_process_of_bound line 31
  4. theorem OAI.Problem367.lipschitzWith_nnrealTimePrimitive line 39
  5. theorem OAI.Problem367.norm_nnrealTimePrimitive_sub_le line 50
  6. theorem OAI.Problem367.innovationCorrection_lipschitzWith line 58
  7. theorem OAI.Problem367.measurable_path_of_isStronglyProgressive line 86
  8. theorem OAI.Problem367.lipschitzWith_nnrealTimePrimitive_of_progressive line 107
  9. theorem OAI.Problem367.innovationCorrection_two_lipschitzWith line 116
  10. def OAI.Problem367.unitClip line 129
  11. theorem OAI.Problem367.continuous_unitClip line 131
  12. theorem OAI.Problem367.norm_unitClip_le line 134
  13. theorem OAI.Problem367.unitClip_eq_of_norm_le line 141
  14. theorem OAI.Problem367.isStronglyProgressive_unitClip line 145
  15. theorem OAI.Problem367.unitClip_posterior_version line 152
  16. theorem OAI.Problem367.exists_pointwise_bounded_progressive_posterior line 163