OAI/Geometry/SurfaceImmersion/Correction/PolynomialQuadrature.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The polynomial Hessian has the same two-quadrature zero-mode identity as the metric Hessian.

  1. lemma OAI.ClosedSurfaceR4.JetPolynomial.complexJet_const_smul line 13
  2. lemma OAI.ClosedSurfaceR4.JetPolynomial.starDirectionJets_const_smul line 20
  3. lemma OAI.ClosedSurfaceR4.JetPolynomial.half_second_variation_quadrature line 25
  4. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.polynomial_quadrature_sum line 45
  5. lemma OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.real_mode_coordinates line 68
  6. theorem OAI.ClosedSurfaceR4.JetPolynomial.Perturbation.coordinate_polynomial_quadrature line 77