OAI/Combinatorics/UniformKServer/TierPilot.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniformKServer.TierPilot.Parameters line 18

   Source documentation

   The two source pilot templates use D_H=51200, R_L=4D_H, D_L=100R_L. The small numerical parameters remain free so the later travel absorption can choose them once and for all.

   structure Parameters where
   …

2. def OAI.UniformKServer.TierPilot.heavy line 34
3. def OAI.UniformKServer.TierPilot.insertionMass line 37
4. structure OAI.UniformKServer.TierPilot.Edit line 44

   Source documentation

   Structural facts of the source short-roster expected parameter at an insertion; its explicit finite-law construction is separate from this local analytic gain. These are ramp/retirement facts, not a pilot gain premise.

   structure Edit (r ε : ℝ) (x : X) (go gn : X → ℝ) : Prop where
   …

5. def OAI.UniformKServer.TierPilot.variation line 51
6. theorem OAI.UniformKServer.TierPilot.Parameters.sigma_le_one line 56
7. theorem OAI.UniformKServer.TierPilot.Parameters.gammaH_pos line 58
8. theorem OAI.UniformKServer.TierPilot.ballMass_nonneg line 61
9. theorem OAI.UniformKServer.TierPilot.annulus_identity line 67
10. theorem OAI.UniformKServer.TierPilot.insertionMass_bounds line 80
11. theorem OAI.UniformKServer.TierPilot.residual_bounds line 91
12. theorem OAI.UniformKServer.TierPilot.variation_nonneg line 98
13. theorem OAI.UniformKServer.TierPilot.variation_mono line 107
14. theorem OAI.UniformKServer.TierPilot.variation_sub line 116
15. theorem OAI.UniformKServer.TierPilot.integrand_variation line 121
16. theorem OAI.UniformKServer.TierPilot.variation_constant_bound line 128
17. theorem OAI.UniformKServer.TierPilot.plateau line 144
18. theorem OAI.UniformKServer.TierPilot.heavy_coefficient_lower line 152
19. theorem OAI.UniformKServer.TierPilot.increasing_site_zero line 189
20. def OAI.UniformKServer.TierPilot.rise line 225
21. def OAI.UniformKServer.TierPilot.fall line 226
22. theorem OAI.UniformKServer.TierPilot.rise_nonneg line 229
23. theorem OAI.UniformKServer.TierPilot.fall_nonneg line 231
24. theorem OAI.UniformKServer.TierPilot.rise_bound line 234
25. theorem OAI.UniformKServer.TierPilot.rise_zero line 239
26. theorem OAI.UniformKServer.TierPilot.rise_support line 243
27. theorem OAI.UniformKServer.TierPilot.rise_nonheavy_point line 250
28. theorem OAI.UniformKServer.TierPilot.rise_heavy_point line 277
29. theorem OAI.UniformKServer.TierPilot.rise_integral_bound line 307
30. theorem OAI.UniformKServer.TierPilot.fall_unit line 337
31. theorem OAI.UniformKServer.TierPilot.fall_near_point line 342
32. theorem OAI.UniformKServer.TierPilot.residual_half line 371
33. theorem OAI.UniformKServer.TierPilot.fall_far_point line 400
34. theorem OAI.UniformKServer.TierPilot.qualification_inner line 419
35. theorem OAI.UniformKServer.TierPilot.fall_integral_bound line 428
36. theorem OAI.UniformKServer.TierPilot.insertion_gain line 488

    Source documentation

    Source tier-pilot drop with explicit absolute constants. The later short-roster bound substitutes ε ≤ C/√K.

    theorem insertion_gain (P : Parameters) (r ε h : ℝ) (hr : 0 < r)
        (hε : 0 ≤ ε) (hh : 1 ≤ h) (μ go gn : X → ℝ) (hμ : ∀ p, 0 ≤ μ p)
        (x : X) (hM : 0 < ballMass r P.gammaH μ x)
        (hqual : ballMass r 20480000 μ x ≤ Real.exp h*ballMass r P.gammaL μ x)
        (he : Edit r ε x go gn) :
        r*insertionMass P r μ x*
          (min (1/2) (128*P.deltaH)*Real.exp (-h)-257*ε) ≤
            value r P.sigma 204800 μ go-value r P.sigma 204800 μ gn
     := by
    …

    Mentions: OAI.UniformKServer.TierPilot.Parameters, OAI.UniformKServer.TierPilot.Edit, OAI.UniformKServer.TierPilot.insertionMass