OAI/MathematicalPhysics/CriticalSK/PathEnergy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.edgeCoeff line 27
  2. def OAI.CriticalSK.pathEnergy line 29
  3. lemma OAI.CriticalSK.path_energy_identity line 33
  4. lemma OAI.CriticalSK.edgeCoeff_nonneg line 59
  5. lemma OAI.CriticalSK.edgeCoeff_last line 61
  6. lemma OAI.CriticalSK.edgeCoeff_upper line 64
  7. lemma OAI.CriticalSK.edgeCoeff_le_one line 77
  8. lemma OAI.CriticalSK.edge_deficit line 80
  9. lemma OAI.CriticalSK.pathEnergy_expansion line 89
  10. lemma OAI.CriticalSK.pathEnergy_controls line 96
  11. lemma OAI.CriticalSK.pathEnergy_nonneg line 104
  12. lemma OAI.CriticalSK.pathEnergy_weighted_mass line 112
  13. lemma OAI.CriticalSK.pathEnergy_weighted_gradient line 128
  14. lemma OAI.CriticalSK.pathEnergy_tail line 136
  15. lemma OAI.CriticalSK.edgeCoeff_lower_half line 151
  16. lemma OAI.CriticalSK.edge_gradient_control line 163
  17. lemma OAI.CriticalSK.pathEnergy_gradient line 187
  18. lemma OAI.CriticalSK.square_weight_variation line 211
  19. lemma OAI.CriticalSK.product_weight_variation line 226
  20. lemma OAI.CriticalSK.pathEnergy_le_four_mass line 244