OAI/Dynamics/EntropyCounterexample/PredictionTerm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem340.norm_fderiv_real_smul_le line 14
  2. lemma OAI.Problem340.norm_fderiv_real_comp_le line 22
  3. def OAI.Problem340.predictionTerm line 29
  4. theorem OAI.Problem340.norm_fderiv_prediction_product_le line 32
  5. theorem OAI.Problem340.norm_prediction_product_le line 75
  6. theorem OAI.Problem340.norm_add_fderiv_prediction_product_le line 90
  7. lemma OAI.Problem340.prediction_growth_absorb line 107
  8. theorem OAI.Problem340.prediction_term_majorant line 113
  9. theorem OAI.Problem340.contDiff_predictionTerm line 135