OAI/Combinatorics/SumProduct/Alignment/RoughReal01.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RoughRealCharacterIdentity.sum_degree line 25
  2. lemma OAI.RoughRealCharacterIdentity.eq_of_integer_agree line 37
  3. def OAI.RoughRealCharacterIdentity.gridMv line 56
  4. lemma OAI.RoughRealCharacterIdentity.eval_gridMv line 59
  5. lemma OAI.RoughRealCharacterIdentity.gridMv_degree line 69
  6. def OAI.RoughRealCharacterIdentity.jointArray line 82
  7. lemma OAI.RoughRealCharacterIdentity.timeCoefficient_jointArray line 86
  8. lemma OAI.RoughRealCharacterIdentity.joint_grid_degree line 96
  9. lemma OAI.RoughRealCharacterIdentity.character_degree line 113
  10. theorem OAI.RoughRealCharacterIdentity.character_identity_real line 127
  11. lemma OAI.RoughRationalBlock.smooth_mul line 169
  12. lemma OAI.RoughRationalBlock.affine_degree line 177
  13. lemma OAI.RoughRationalBlock.int_interval_card line 183
  14. def OAI.RoughRationalBlock.Split line 189
  15. theorem OAI.RoughRationalBlock.eventual_split line 204