OAI/Analysis/PlanarPacking/Quadrature.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpPlanar.cheb_primitive_deriv line 17
  2. lemma OAI.SharpPlanar.cheb_integral line 34
  3. lemma OAI.SharpPlanar.fejer_recip_telescope line 62
  4. lemma OAI.SharpPlanar.fejer_recip_sum line 71
  5. lemma OAI.SharpPlanar.fejerWeight_pos line 83
  6. def OAI.SharpPlanar.fejerPolynomial line 100
  7. lemma OAI.SharpPlanar.fejerPolynomial_eval line 103
  8. lemma OAI.SharpPlanar.fejerPolynomial_degree line 117
  9. lemma OAI.SharpPlanar.fejer_weighted_orthogonal line 130
  10. lemma OAI.SharpPlanar.fejer_integral_zero line 144
  11. lemma OAI.SharpPlanar.fejer_integral_even line 158
  12. lemma OAI.SharpPlanar.fejer_integral_odd line 180
  13. lemma OAI.SharpPlanar.fejer_cheb_integral line 195
  14. lemma OAI.SharpPlanar.fejer_polynomial_integral line 215
  15. lemma OAI.SharpPlanar.fejer_exact line 238
  16. lemma OAI.SharpPlanar.fejer_mass line 269
  17. lemma OAI.SharpPlanar.fejerNode_mem line 274
  18. lemma OAI.SharpPlanar.fejer_exact_monomial line 277
  19. lemma OAI.SharpPlanar.fejer_exact_complex line 286
  20. lemma OAI.SharpPlanar.geometric_tail_error line 315
  21. def OAI.SharpPlanar.taylorPolynomial line 333
  22. lemma OAI.SharpPlanar.analytic_taylor_error line 336
  23. lemma OAI.SharpPlanar.positive_quadrature_error line 364
  24. lemma OAI.SharpPlanar.taylorPolynomial_zero line 404
  25. lemma OAI.SharpPlanar.fejer_analytic_average_error line 410
  26. def OAI.SharpPlanar.diskAffine line 475
  27. lemma OAI.SharpPlanar.diskAffine_mem line 476
  28. lemma OAI.SharpPlanar.finiteDensity_differentiable line 481
  29. lemma OAI.SharpPlanar.complexDirectFactor_differentiable line 485
  30. lemma OAI.SharpPlanar.complexLambda_differentiableAt line 489
  31. lemma OAI.SharpPlanar.complexZ_differentiableAt line 493
  32. lemma OAI.SharpPlanar.complexTransformedFactor_differentiableAt line 497
  33. lemma OAI.SharpPlanar.directIntegrand_analytic line 505
  34. lemma OAI.SharpPlanar.transformedIntegrand_analytic line 513
  35. lemma OAI.SharpPlanar.directMoment_piece_average_error line 526
  36. lemma OAI.SharpPlanar.transformedMoment_piece_average_error line 540
  37. def OAI.SharpPlanar.pieceIntegral line 559
  38. def OAI.SharpPlanar.pieceRule line 561
  39. lemma OAI.SharpPlanar.pieceIntegral_affine line 565
  40. lemma OAI.SharpPlanar.piece_rule_error_scaling line 586
  41. lemma OAI.SharpPlanar.directMoment_piece_error line 598
  42. lemma OAI.SharpPlanar.transformedMoment_piece_error line 607
  43. lemma OAI.SharpPlanar.six_piece_error line 616
  44. lemma OAI.SharpPlanar.directMoment_rule_error line 626
  45. lemma OAI.SharpPlanar.transformedMoment_rule_error line 635
  46. def OAI.SharpPlanar.singleCoefficient line 649
  47. lemma OAI.SharpPlanar.singleCoefficient_mass line 650
  48. lemma OAI.SharpPlanar.singleDensity_u line 653
  49. lemma OAI.SharpPlanar.singleDensity_v line 656
  50. def OAI.SharpPlanar.complexBasis line 660
  51. def OAI.SharpPlanar.complexBasisMoment line 662
  52. lemma OAI.SharpPlanar.complexBasis_rule_error line 665