OAI/Combinatorics/Progressions/Lattices/JointAffineL1Parameter.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.affineProductProfile_range_bound line 16
  2. theorem OAI.Erdos3.affineCoefficientDensity_split line 25
  3. def OAI.Erdos3.affineSelectedJetDensity line 64
  4. theorem OAI.Erdos3.affineSelectedJetDensity_bounds line 74
  5. def OAI.Erdos3.affineJetL1Cost line 115
  6. theorem OAI.Erdos3.affineSelectedJetDensity_l1_regular line 120
  7. theorem OAI.Erdos3.affineSelectedJetDensity_principalTuple_riemann line 162
  8. theorem OAI.Erdos3.splitPivotDensity_output_lipschitz line 206
  9. theorem OAI.Erdos3.affineSelectedJetDensity_output_lipschitz line 227
  10. theorem OAI.Erdos3.affineSelectedJetDensity_output_cap line 246
  11. theorem OAI.Erdos3.affineSelectedJetDensity_output_support line 270
  12. def OAI.Erdos3.jointAffineJetDensity line 298
  13. theorem OAI.Erdos3.jointAffineJetDensity_bounds line 308
  14. def OAI.Erdos3.affineJetL1Log line 350
  15. theorem OAI.Erdos3.affineJetL1Log_nonneg line 354
  16. theorem OAI.Erdos3.affineJetL1Cost_le_exp line 359
  17. def OAI.Erdos3.affineSelectedJetProfile line 397
  18. theorem OAI.Erdos3.affineSelectedJetProfile_probability_data line 403
  19. theorem OAI.Erdos3.jointAffineJetDensity_law line 427
  20. theorem OAI.Erdos3.jointAffineJetDensity_probability_data line 458
  21. theorem OAI.Erdos3.jointAffineJetDensity_measurable_comp line 494
  22. theorem OAI.Erdos3.affineSelectedJetDensity_probability_data line 531
  23. theorem OAI.Erdos3.jointAffineJetDensity_l1_regular line 545