OAI/Geometry/Cannon/ScalarLimits/OscillationPairwise.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonScalarEnergy.oscillation_le_of_pairwise line 27
2. lemma OAI.CannonScalarEnergy.oscillation_nonneg_of_compact line 38
3. theorem OAI.CannonScalarEnergy.uniform_local_energy_bound line 45
4. theorem OAI.CannonApprox.exists_scalar_energy_constant line 94
5. theorem OAI.CannonApprox.exists_scalar_of_crossing_modulus line 129