OAI/Combinatorics/UniformKServer/HeavyPilot.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.HeavyPilot.ramp line 16

   Source documentation

   The clipped ramp on [3,4].

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

2. def OAI.UniformKServer.HeavyPilot.parameter line 19

   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. def OAI.UniformKServer.HeavyPilot.updateCenters line 23

   Source documentation

   The heavy update deletes all centers at distance at most 100r, then inserts x.

   def updateCenters (r : ℝ) (H : Finset X) (x : X) : Finset X :=
   …

4. def OAI.UniformKServer.HeavyPilot.annulusMass line 26
5. theorem OAI.UniformKServer.HeavyPilot.ramp_bounds line 36
6. theorem OAI.UniformKServer.HeavyPilot.ramp_zero line 40
7. theorem OAI.UniformKServer.HeavyPilot.ramp_one line 44
8. theorem OAI.UniformKServer.HeavyPilot.ramp_lip line 50
9. theorem OAI.UniformKServer.HeavyPilot.parameter_bounds line 57
10. theorem OAI.UniformKServer.HeavyPilot.parameter_le_center line 68
11. theorem OAI.UniformKServer.HeavyPilot.le_parameter line 72
12. theorem OAI.UniformKServer.HeavyPilot.parameter_lip line 81
13. theorem OAI.UniformKServer.HeavyPilot.update_zero line 106
14. theorem OAI.UniformKServer.HeavyPilot.update_far line 112
15. theorem OAI.UniformKServer.HeavyPilot.increase_support line 127
16. theorem OAI.UniformKServer.HeavyPilot.near_old_one line 138
17. theorem OAI.UniformKServer.HeavyPilot.near_new_zero line 152
18. theorem OAI.UniformKServer.HeavyPilot.annulus_surcharge line 158
19. theorem OAI.UniformKServer.HeavyPilot.integrand_gain line 182
20. theorem OAI.UniformKServer.HeavyPilot.heavy_gain line 247

    Source documentation

    Exact heavy-center pilot gain, companion §07 heavy annulus budget.

    theorem heavy_gain (r γ δ : ℝ) (hr : 0 < r)
        (hγ : 0 < γ) (hγsmall : γ ≤ 1/64) (hδ : 0 < δ) (hδsmall : δ ≤ 1/4112)
        (μ : X → ℝ) (hμ : ∀ p, 0 ≤ μ p) (H : Finset X) (x : X)
        (hfar : ∀ c ∈ H, 8*r < dist x c)
        (hM : 0 < ballMass r γ μ x)
        (hconc : ballMass r (100*512) μ x ≤ (1+δ)*ballMass r γ μ x) :
        127*r*annulusMass r μ x ≤
          value r 1 512 μ (parameter r H) -
            value r 1 512 μ (parameter r (updateCenters r H x))
     := by
    …

    Mentions: OAI.UniformKServer.HeavyPilot.annulusMass, OAI.UniformKServer.HeavyPilot.parameter, OAI.UniformKServer.HeavyPilot.updateCenters