OAI/Combinatorics/Progressions/Lattices/NativeSampleVerticalAffineExpansion.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeSampleModel.affineRestrictionTest line 20
  2. theorem OAI.Erdos3.NativeSampleModel.affineRestrictionTest_eval line 25
  3. theorem OAI.Erdos3.NativeSampleModel.exists_affineRestriction_family line 34
  4. theorem OAI.Erdos3.BooleanCubeKernel.jointIntegerPhysicalSite_eq_integerAffineMap line 54
  5. theorem OAI.Erdos3.NativeSampleModel.exists_jointPhysicalRestriction_family line 67
  6. def OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent line 107
  7. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_observable line 111
  8. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_orbit line 114
  9. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_normBound line 121
  10. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_lipBound line 124
  11. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_complexity line 127
  12. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_normBound_le line 130
  13. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_vertical line 133
  14. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_integral line 141
  15. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_preserves_character line 148
  16. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_eval line 155
  17. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_eval_error line 160
  18. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_sample_error line 166
  19. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.affineComponent_norm_eval_le line 172
  20. def OAI.Erdos3.NativeSampleModel.VerticalExpansion.jointPhysicalComponent line 183
  21. theorem OAI.Erdos3.NativeSampleModel.VerticalExpansion.jointPhysicalComponent_error line 189