OAI/Computability/MinUncut/Estimates/Convolution.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.GaussianHermite.noise_derivative line 17
  2. def OAI.MinUncut.GaussianHermite.convolution line 37
  3. def OAI.MinUncut.GaussianHermite.convolutionGradient line 40
  4. lemma OAI.MinUncut.GaussianHermite.convolution_derivative line 43
  5. lemma OAI.MinUncut.GaussianHermite.convolution_as_noise line 50
  6. lemma OAI.MinUncut.GaussianHermite.convolutionGradient_as_noise line 62
  7. lemma OAI.MinUncut.GaussianHermite.convolution_poincare line 77
  8. lemma OAI.MinUncut.GaussianHermite.convolution_gradient_tail line 86
  9. lemma OAI.MinUncut.RowNoise.expect_prod line 105
  10. def OAI.MinUncut.RowNoise.rowDensity line 110
  11. lemma OAI.MinUncut.RowNoise.rowDensity_mean line 114
  12. lemma OAI.MinUncut.RowNoise.rowDensity_symmetric line 124
  13. lemma OAI.MinUncut.RowNoise.rowDensity_nonneg line 128
  14. def OAI.MinUncut.RowNoise.density line 133
  15. lemma OAI.MinUncut.RowNoise.density_mean line 136
  16. lemma OAI.MinUncut.RowNoise.density_symmetric line 140
  17. lemma OAI.MinUncut.RowNoise.density_nonneg line 144
  18. def OAI.MinUncut.RowNoise.frequency line 147
  19. lemma OAI.MinUncut.RowNoise.dual_apply line 151
  20. lemma OAI.MinUncut.RowNoise.sign_sum line 159
  21. lemma OAI.MinUncut.RowNoise.character_product line 167
  22. def OAI.MinUncut.RowNoise.mask line 171
  23. def OAI.MinUncut.RowNoise.degree line 174
  24. lemma OAI.MinUncut.RowNoise.row_character_eigen line 176
  25. def OAI.MinUncut.RowNoise.noise line 191
  26. lemma OAI.MinUncut.RowNoise.noise_character line 194
  27. lemma OAI.MinUncut.RowNoise.noise_expansion line 204
  28. lemma OAI.MinUncut.RowNoise.correlation line 220
  29. lemma OAI.MinUncut.RowNoise.stationary line 234
  30. lemma OAI.MinUncut.RowNoise.dirichlet line 241
  31. def OAI.MinUncut.RowNoise.project line 258
  32. lemma OAI.MinUncut.RowNoise.coefficient_project line 262
  33. lemma OAI.MinUncut.RowNoise.coefficient_residual line 270
  34. lemma OAI.MinUncut.RowNoise.residual_energy line 280
  35. lemma OAI.MinUncut.RowNoise.geometric_bernoulli line 290
  36. lemma OAI.MinUncut.RowNoise.spectral_weight_ge_one line 303
  37. lemma OAI.MinUncut.RowNoise.row_tail_le line 309