OAI/Geometry/WeakMTW/Potentials/IntermediateUniformBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WeakMTWGlobalSupport.WeakMTW.cost_family_bounds line 28
2. def OAI.WeakMTWGlobalSupport.WeakMTW.intermediateCenter line 53
3. def OAI.WeakMTWGlobalSupport.WeakMTW.intermediateUpperCost line 54
4. def OAI.WeakMTWGlobalSupport.WeakMTW.intermediateLowerCost line 56
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.intermediateCenter_continuous line 59
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.intermediate_local_support_bounds line 67
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.intermediate_uniform_support_bounds line 102