OAI/Geometry/LatticeCovering/Residuals.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Vertical.suffixBinary_fixed line 43
  2. lemma OAI.SingleLatticeCovering.Vertical.gamma_unit_box line 59
  3. def OAI.SingleLatticeCovering.Vertical.Chain.FullResidual line 73
  4. def OAI.SingleLatticeCovering.Vertical.Chain.FullSelected line 79
  5. theorem OAI.SingleLatticeCovering.Vertical.Chain.full_patterns line 87
  6. lemma OAI.SingleLatticeCovering.Vertical.gamma_le_one line 137
  7. lemma OAI.SingleLatticeCovering.Vertical.Chain.dim_last_le line 150
  8. lemma OAI.SingleLatticeCovering.Vertical.Chain.last_le_first line 158
  9. lemma OAI.SingleLatticeCovering.Vertical.Chain.every_le_first line 166
  10. lemma OAI.SingleLatticeCovering.Vertical.Chain.blockSum_dim line 172
  11. def OAI.SingleLatticeCovering.Vertical.Chain.heights line 177
  12. def OAI.SingleLatticeCovering.Vertical.Chain.radiusSq line 181
  13. lemma OAI.SingleLatticeCovering.Vertical.Chain.heights_square_sum line 183
  14. lemma OAI.SingleLatticeCovering.Vertical.Chain.residual_physical line 191
  15. lemma OAI.SingleLatticeCovering.Vertical.Chain.heights_nonneg line 202
  16. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_residual_square line 211
  17. def OAI.SingleLatticeCovering.Vertical.Chain.AtomBound line 234
  18. lemma OAI.SingleLatticeCovering.Vertical.Chain.selected_cap line 238
  19. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_selected_cap line 254
  20. lemma OAI.SingleLatticeCovering.Vertical.gamma1_le_one line 275
  21. lemma OAI.SingleLatticeCovering.Vertical.Chain.blockSum_add line 282
  22. lemma OAI.SingleLatticeCovering.Vertical.Chain.radius_bound line 288
  23. lemma OAI.SingleLatticeCovering.Vertical.Chain.coefficient_half line 341
  24. lemma OAI.SingleLatticeCovering.Vertical.Chain.terminal_bound line 372
  25. theorem OAI.SingleLatticeCovering.Vertical.vertical_patterns_core line 404
  26. lemma OAI.SingleLatticeCovering.Vertical.Block.shiftDim_bound line 516
  27. lemma OAI.SingleLatticeCovering.Vertical.Block.shift_bound line 538
  28. lemma OAI.SingleLatticeCovering.Vertical.succ_le_two_power line 543
  29. lemma OAI.SingleLatticeCovering.Vertical.inverse_factor_bound line 548
  30. lemma OAI.SingleLatticeCovering.Vertical.Chain.injectLast_bound line 559
  31. lemma OAI.SingleLatticeCovering.Vertical.Chain.inverse_coordinate_bound line 569
  32. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_inverse_coordinate_bound line 636
  33. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_residual_physical line 682
  34. def OAI.SingleLatticeCovering.Vertical.Chain.alphabetRadius line 694
  35. lemma OAI.SingleLatticeCovering.Vertical.Chain.raw_coordinate_bound line 697
  36. def OAI.SingleLatticeCovering.Vertical.Chain.denominators line 712
  37. def OAI.SingleLatticeCovering.Vertical.Chain.fullDenominators line 716
  38. lemma OAI.SingleLatticeCovering.Vertical.Chain.denominators_pos line 719
  39. lemma OAI.SingleLatticeCovering.Vertical.Chain.raw_rational line 727
  40. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_raw_rational line 742
  41. def OAI.SingleLatticeCovering.Vertical.rationalAlphabet line 758
  42. lemma OAI.SingleLatticeCovering.Vertical.mem_rationalAlphabet line 761
  43. lemma OAI.SingleLatticeCovering.Vertical.rationalAlphabet_card line 773
  44. def OAI.SingleLatticeCovering.Vertical.Chain.alphabets line 780
  45. lemma OAI.SingleLatticeCovering.Vertical.Chain.mem_alphabets line 783