OAI/Probability/GaussianPropeller/Deletion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussianPropeller.Reduction.optimal_width_le line 14
  2. lemma OAI.GaussianPropeller.Reduction.erase_univ_nonempty line 27
  3. def OAI.GaussianPropeller.Reduction.omittedMax line 34
  4. def OAI.GaussianPropeller.Reduction.recentered line 38
  5. lemma OAI.GaussianPropeller.Reduction.sum_erase_zero line 42
  6. lemma OAI.GaussianPropeller.Reduction.sum_erased_centered line 50
  7. lemma OAI.GaussianPropeller.Reduction.recentered_norm_sq line 62
  8. lemma OAI.GaussianPropeller.Reduction.scoreMax_recentered line 96
  9. lemma OAI.GaussianPropeller.Reduction.omittedMax_integrable line 128
  10. lemma OAI.GaussianPropeller.Reduction.integral_omittedMax line 140
  11. lemma OAI.GaussianPropeller.Reduction.scoreMax_eq_max_omitted line 155
  12. lemma OAI.GaussianPropeller.Reduction.positive_gap_eq line 170
  13. theorem OAI.GaussianPropeller.Reduction.optimal_loss_lower line 176