OAI/Dynamics/EntropyCounterexample/MapRegularity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.Construction.inputAngularFactor line 11
2. theorem OAI.Problem340.Construction.baseInput_eq_predictionSummand_tsum line 14
3. theorem OAI.Problem340.Construction.exists_cutoff_fderiv_bound line 28
4. theorem OAI.Problem340.Construction.norm_inputAngularFactor_le_one line 46
5. theorem OAI.Problem340.Construction.contDiffOn_baseInput_of_chart_bounds line 52
6. theorem OAI.Problem340.Construction.contDiffOn_baseInput_of_scaled_chart_bounds line 97