OAI/Geometry/SmoothYau/Estimates/ComplexGaussianRealValue.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.complex_stdGaussian_eq_map line 44
  2. lemma OAI.YauCounterexamples.complex_gaussian_pair line 50
  3. lemma OAI.YauCounterexamples.gaussian_complex_rotation line 59
  4. lemma OAI.YauCounterexamples.gaussian_complex_conj line 63
  5. lemma OAI.YauCounterexamples.gaussian_complex_pi_rotation line 67
  6. lemma OAI.YauCounterexamples.gaussian_complex_from_real_parts line 72
  7. def OAI.YauCounterexamples.selectedCoefficientOrder line 88
  8. def OAI.YauCounterexamples.selectedComplexCoefficients line 101
  9. lemma OAI.YauCounterexamples.selectedComplexCoefficients_law line 106
  10. theorem OAI.YauCounterexamples.stdGaussian_opposite_eq line 132
  11. theorem OAI.YauCounterexamples.gaussian_wave_opposite_uniform line 160
  12. def OAI.YauCounterexamples.complexGaussianRealValue line 181
  13. lemma OAI.YauCounterexamples.complexGaussianRealValue_real_parts line 184
  14. lemma OAI.YauCounterexamples.complex_gaussian_standardized_sign_law line 194
  15. theorem OAI.YauCounterexamples.complex_gaussian_sign_uniform line 234