OAI/Combinatorics/Progressions/Estimates/RealifiedReconstruction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.weightedLinearInverseMask line 12
  2. theorem OAI.Erdos3.weightedLinearInverseMask_apply line 19
  3. theorem OAI.Erdos3.weightedLinearInverseMask_entry line 30
  4. theorem OAI.Erdos3.weightedLinearInverseMask_weighted line 47
  5. theorem OAI.Erdos3.weightedLinearInverseMask_height line 53
  6. theorem OAI.Erdos3.exists_bounded_linear_section line 77
  7. theorem OAI.Erdos3.linearMap_baseChange_basis line 97
  8. theorem OAI.Erdos3.linearMap_baseChange_rightInverse line 104
  9. theorem OAI.Erdos3.exists_bounded_realified_linear_section line 113
  10. theorem OAI.Erdos3.exists_bounded_rational_image_section line 137
  11. theorem OAI.Erdos3.exists_bounded_linear_image_section line 184
  12. theorem OAI.Erdos3.linearMap_baseChange_image_section line 202
  13. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_filtered_section line 222
  14. theorem OAI.Erdos3.exists_controlled_coordinate_leftInverse line 310
  15. theorem OAI.Erdos3.exists_controlled_weighted_leftInverse line 329
  16. def OAI.Erdos3.rationalReconstructionLipschitzBound line 356
  17. theorem OAI.Erdos3.realificationMap_lattice_cover line 368
  18. theorem OAI.Erdos3.exists_lipschitz_realification_reconstruction line 383