OAI/Geometry/Cannon/Modulus/RadialCellEnergy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonRadialEnergy.radial_cell_energy line 20
  2. theorem OAI.CannonRadialEnergy.radial_cell_energy_budget line 47
  3. theorem OAI.CannonRadialEnergy.disjoint_disk_square_budget line 66
  4. theorem OAI.CannonRadialEnergy.disk_realization_radial_energy line 98
  5. theorem OAI.CannonRadialEnergy.disk_radial_modulus_lower line 123
  6. lemma OAI.CannonCells.indices_image_preimage line 174
  7. theorem OAI.CannonCells.modulus_image_preimage line 185
  8. theorem OAI.CannonRadialEnergy.source_radial_modulus_lower line 206
  9. theorem OAI.CannonTransfer.overlap_energy line 253
  10. lemma OAI.CannonCarrierCharging.sum_le_charges line 300
  11. theorem OAI.CannonCarrierCharging.path_cell_charging line 319
  12. theorem OAI.CannonCarrierCharging.carrier_admissible_charging line 349
  13. theorem OAI.CannonCarrierCharging.radial_carrier_modulus_bound line 379