OAI/MathematicalPhysics/DefocusingNLS/Certificates/BoundaryHornerTransform.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Sound homogeneous Horner transforms for the three certificate charts

  1. def OAI.DefocusingNLS.BoundaryCertificate.chartNumerator line 12
  2. def OAI.DefocusingNLS.BoundaryCertificate.chartDenominator line 13
  3. def OAI.DefocusingNLS.BoundaryCertificate.polynomialTransformAux line 15
  4. def OAI.DefocusingNLS.BoundaryCertificate.homogeneousHorner line 21
  5. theorem OAI.DefocusingNLS.BoundaryCertificate.chartNumerator_sound line 25
  6. theorem OAI.DefocusingNLS.BoundaryCertificate.chartDenominator_sound line 31
  7. theorem OAI.DefocusingNLS.BoundaryCertificate.polynomialTransformAux_append line 35
  8. theorem OAI.DefocusingNLS.BoundaryCertificate.polynomialTransformAux_second line 43
  9. theorem OAI.DefocusingNLS.BoundaryCertificate.polynomialTransformAux_reverse line 53
  10. theorem OAI.DefocusingNLS.BoundaryCertificate.transformAux_sound line 64