OAI/MathematicalPhysics/PEPSSubvolume/Interpolation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Three-lines tangent estimates for entropy derivatives.

  1. theorem OAI.PolynomialPEPS.Subvolume.FilterInterpolation.deriv_le_of_right_comparison line 26
  2. theorem OAI.PolynomialPEPS.Subvolume.FilterInterpolation.threeLines_tangent_zero line 42
  3. theorem OAI.PolynomialPEPS.Subvolume.FilterInterpolation.entropy_cost_upper_of_spectral_curve line 66