OAI/MathematicalPhysics/PEPSSubvolume/NestedLower.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Reoptimized prefix costs and nested entropy lower comparisons.

  1. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.ordered_product_succ line 27
  2. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.filtered_vector_succ line 34
  3. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.optimized_prefix_amplitude line 42
  4. theorem OAI.PolynomialPEPS.Subvolume.PrefixLower.optimized_prefix_overlap line 64
  5. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.curve_isUnit line 87
  6. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.norm_asMap_pos line 94
  7. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.optimizer_norm_pos line 106
  8. def OAI.PolynomialPEPS.Subvolume.NestedLower.extend line 133
  9. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.extend_fin line 137
  10. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.optimizer_half_fidelity line 141
  11. lemma OAI.PolynomialPEPS.Subvolume.NestedLower.boundary_budget_mono line 187
  12. theorem OAI.PolynomialPEPS.Subvolume.NestedLower.optimizer_norm_bound line 193
  13. theorem OAI.PolynomialPEPS.Subvolume.NestedLower.optimizer_entropy_lower line 257