OAI/Probability/UnimodularPercolation/Subdivision/Operator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Operator bounds transferred through graph subdivision.

  1. theorem OAI.Percolation.sum_inl_extend_le line 20
  2. def OAI.Percolation.hilbertInlValue line 29
  3. theorem OAI.Percolation.norm_hilbertInlValue_le line 32
  4. def OAI.Percolation.hilbertInl line 35
  5. theorem OAI.Percolation.hilbertInl_apply_inl line 54
  6. theorem OAI.Percolation.hilbertInl_apply_inr line 56
  7. theorem OAI.Percolation.sum_inl_restrict_le line 59
  8. def OAI.Percolation.hilbertRestrictInlValue line 65
  9. theorem OAI.Percolation.norm_hilbertRestrictInlValue_le line 68
  10. def OAI.Percolation.hilbertRestrictInl line 72
  11. theorem OAI.Percolation.hilbertRestrictInl_apply line 79
  12. theorem OAI.Percolation.hilbertInl_single line 82
  13. theorem OAI.Percolation.operatorBounded_of_subdivision line 89
  14. theorem OAI.Percolation.critical_bounded_of_subdivision line 106