OAI/Dynamics/EntropyCounterexample/PredictionTerm.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Problem340.norm_fderiv_real_smul_leline 14 - lemma
OAI.Problem340.norm_fderiv_real_comp_leline 22 - def
OAI.Problem340.predictionTermline 29 - theorem
OAI.Problem340.norm_fderiv_prediction_product_leline 32 - theorem
OAI.Problem340.norm_prediction_product_leline 75 - theorem
OAI.Problem340.norm_add_fderiv_prediction_product_leline 90 - lemma
OAI.Problem340.prediction_growth_absorbline 107 - theorem
OAI.Problem340.prediction_term_majorantline 113 - theorem
OAI.Problem340.contDiff_predictionTermline 135