OAI/Combinatorics/UniformKServer/HeavyEditRamp.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.HeavyEditRamp.ramp line 15

   Source documentation

   The clipped ramp on [9,10].

   def ramp (v : ℝ) : ℝ := max 0 (min 1 (v-9))

2. def OAI.UniformKServer.HeavyEditRamp.parameter line 18

   Source documentation

   The source's ramp of distance to the center set, equal to one for the empty set.

   def parameter (r : ℝ) (H : Finset X) (p : X) : ℝ :=
   …

3. theorem OAI.UniformKServer.HeavyEditRamp.ramp_bounds line 28
4. theorem OAI.UniformKServer.HeavyEditRamp.ramp_zero line 32
5. theorem OAI.UniformKServer.HeavyEditRamp.ramp_one line 36
6. theorem OAI.UniformKServer.HeavyEditRamp.ramp_lip line 42
7. theorem OAI.UniformKServer.HeavyEditRamp.parameter_bounds line 49
8. theorem OAI.UniformKServer.HeavyEditRamp.parameter_le_center line 60
9. theorem OAI.UniformKServer.HeavyEditRamp.le_parameter line 64
10. theorem OAI.UniformKServer.HeavyEditRamp.parameter_lip line 73
11. theorem OAI.UniformKServer.HeavyEditRamp.center_zero line 102
12. theorem OAI.UniformKServer.HeavyEditRamp.far_one line 108
13. theorem OAI.UniformKServer.HeavyEditRamp.update_zero line 115
14. theorem OAI.UniformKServer.HeavyEditRamp.update_far line 119