OAI/Computability/MinUncut/Analysis/Gradient.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MinUncut.GaussianHermite.mem_range_bump line 17
2. lemma OAI.MinUncut.GaussianHermite.productHermiteBasis_apply line 31
3. lemma OAI.MinUncut.GaussianHermite.coeff_eq_inner line 35
4. lemma OAI.MinUncut.GaussianHermite.hasSum_coeff_sq line 40
5. lemma OAI.MinUncut.GaussianHermite.parseval line 49
6. lemma OAI.MinUncut.GaussianHermite.coeff_const_mul line 52
7. def OAI.MinUncut.GaussianHermite.gradient line 60
8. lemma OAI.MinUncut.GaussianHermite.memLp_gradient line 63
9. lemma OAI.MinUncut.GaussianHermite.gradient_coefficient line 67
10. lemma OAI.MinUncut.GaussianHermite.gradient_coefficient_sq line 80
11. lemma OAI.MinUncut.GaussianHermite.hasSum_gradient_energy_coord line 91
12. lemma OAI.MinUncut.GaussianHermite.hasSum_gradient_energy line 103
13. lemma OAI.MinUncut.GaussianHermite.memLp_noise line 111
14. lemma OAI.MinUncut.GaussianHermite.coeff_noise line 116
15. lemma OAI.MinUncut.GaussianHermite.coeff_noise_sq line 120
16. lemma OAI.MinUncut.GaussianHermite.psi_zero line 125
17. lemma OAI.MinUncut.GaussianHermite.coeff_zero line 128
18. lemma OAI.MinUncut.GaussianHermite.degree_eq_zero_iff line 131
19. lemma OAI.MinUncut.GaussianHermite.poincare line 135
20. def OAI.MinUncut.GaussianHermite.low line 157
21. lemma OAI.MinUncut.GaussianHermite.mem_low line 160
22. def OAI.MinUncut.GaussianHermite.project line 171
23. lemma OAI.MinUncut.GaussianHermite.memLp_project line 174
24. lemma OAI.MinUncut.GaussianHermite.coeff_project line 178
25. lemma OAI.MinUncut.GaussianHermite.coeff_sub line 190
26. lemma OAI.MinUncut.GaussianHermite.coeff_residual line 197
27. lemma OAI.MinUncut.GaussianHermite.hasSum_gradient_tail_coord line 203
28. lemma OAI.MinUncut.GaussianHermite.hasSum_gradient_tail line 225
29. lemma OAI.MinUncut.GaussianHermite.gradient_tail_le line 237
30. lemma OAI.MinUncut.GaussianHermite.exists_cutoff line 258