OAI/MathematicalPhysics/PEPSSubvolume/PhysicalCurve.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Actual complex filter curves, boundary bounds and positive norms.

  1. def OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitudeCLM line 31
  2. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitudeCLM_apply line 35
  3. def OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve line 43
  4. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve_zero line 46
  5. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve_succ line 47
  6. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve_at_zero line 51
  7. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.hasDerivAt_liftCurve line 56
  8. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.differentiable_prefixCurve line 64
  9. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.hasDerivAt_prefixCurve_zero line 72
  10. def OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude line 88
  11. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude_zero line 91
  12. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.differentiable_amplitude line 96
  13. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.hasDerivAt_amplitude_zero line 100
  14. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve_unitary line 109
  15. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude_left line 114
  16. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.norm_prefixCurve_le_one line 121
  17. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude_stripBound line 137
  18. def OAI.PolynomialPEPS.Subvolume.PhysicalCurve.powerRates line 161
  19. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.powerRates_nonpos line 165
  20. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude_right_of_optimizer line 175
  21. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.curve_isUnit line 217
  22. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.prefixCurve_isUnit line 225
  23. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.norm_asMap_pos_of_isUnit line 233
  24. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.optimizer_norm_pos line 247
  25. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.optimizer_cost_le_trace_rates line 273