OAI/Analysis/IntegralMeans/Moments.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.differentiableOn_classReciprocal line 26
  2. lemma OAI.Brennan.continuous_classReciprocal_eval line 30
  3. def OAI.Brennan.reciprocalJet line 36
  4. lemma OAI.Brennan.continuous_reciprocalJet line 40
  5. lemma OAI.Brennan.continuous_reciprocalJet_eval line 54
  6. lemma OAI.Brennan.classReciprocal_at_I line 58
  7. lemma OAI.Brennan.hasDerivAt_integral_compact line 61
  8. lemma OAI.Brennan.complex_line_deriv line 91
  9. def OAI.Brennan.normFirst line 100
  10. def OAI.Brennan.normSecond line 102
  11. lemma OAI.Brennan.norm_line_hasDerivAt line 105
  12. lemma OAI.Brennan.norm_first_hasDerivAt line 111
  13. lemma OAI.Brennan.norm_first_one line 118
  14. lemma OAI.Brennan.norm_first_I line 121
  15. lemma OAI.Brennan.norm_second_laplacian line 124
  16. lemma OAI.Brennan.continuous_normFirst line 133
  17. lemma OAI.Brennan.continuous_normSecond line 137
  18. def OAI.Brennan.complexLine line 141
  19. def OAI.Brennan.lineDomain line 143
  20. lemma OAI.Brennan.isOpen_lineDomain line 145
  21. lemma OAI.Brennan.complexLine_im line 148
  22. lemma OAI.Brennan.complexLine_mem line 151
  23. lemma OAI.Brennan.complexLine_zero line 154
  24. lemma OAI.Brennan.zero_mem_lineDomain line 155
  25. lemma OAI.Brennan.continuousOn_complexLine line 157
  26. lemma OAI.Brennan.continuous_prod_section line 170
  27. lemma OAI.Brennan.continuousOn_normFirst_line line 176
  28. lemma OAI.Brennan.integral_norm_line_derivative line 184
  29. lemma OAI.Brennan.integral_normFirst_line_derivative line 203
  30. lemma OAI.Brennan.normFirst_expected line 229
  31. lemma OAI.Brennan.compact_holomorphic_line_moments line 248
  32. lemma OAI.Brennan.compact_holomorphic_moments line 275
  33. lemma OAI.Brennan.class_logarithmicJet_I line 318
  34. lemma OAI.Brennan.continuous_root_logarithmicJet line 322
  35. lemma OAI.Brennan.root_logarithmicJet_bounded line 328
  36. lemma OAI.Brennan.weighted_law_moments line 332
  37. lemma OAI.Brennan.jacobian_expectation_nonpos line 359
  38. lemma OAI.Brennan.jacobian_expectation_value line 383
  39. theorem OAI.Brennan.transferRho_le_two line 410