OAI/Analysis/AncientFlat/Evolution/RowContinuity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourceFrozenOrder.normalized_one line 13
  2. lemma OAI.SourceFrozenOrder.integrable_normalized_one line 18
  3. lemma OAI.SourceFrozenOrder.exists_norm_difference_bound line 31
  4. lemma OAI.SourceFrozenOrder.continuous_value line 65
  5. def OAI.SourceFrozenOrder.bcf line 71
  6. lemma OAI.SourceFrozenOrder.bcf_apply line 79
  7. lemma OAI.SourceFrozenOrder.continuousAt_of_value line 83
  8. def OAI.SourceFrozenRows.realCoefficient line 112
  9. lemma OAI.SourceFrozenRows.continuous_realCoefficient line 115
  10. lemma OAI.SourceFrozenRows.row_eq_order_scaled line 120
  11. def OAI.SourceFrozenRows.timeBCF line 130
  12. lemma OAI.SourceFrozenRows.timeBCF_apply line 137
  13. lemma OAI.SourceFrozenRows.continuous_timeBCF line 143