PilotExtension.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.UniformKServer.PilotCompact.weighted_radial_lipschitz line 12

Source documentation

Capacity controls all radii whose support meets either of two nearby points. This is a weighted finite-sum statement, not an assumed HST drift estimate.

theorem weighted_radial_lipschitz (r R a C B : ℝ) (hr : 0 < r) (hR : 256 ≤ R)
    (ha : a ≤ 2*R) (hC : 0 ≤ C) (hB : 0 ≤ B)
    (f : ℝ → ℝ) (hfzero : ∀ u, a ≤ u → f u = 0)
    (hfLip : ∀ u v, 0 ≤ u → 0 ≤ v → |f u-f v| ≤ C*|u-v|)
    (z θ : X → ℝ) (hz : ∀ s, 0 ≤ z s) (hθ : ∀ s, θ s ∈ Set.Icc (0:ℝ) B)
    (x y : X) (hcap : (∑ s, max (z s-gate R (dist s x/r)) 0) ≤ 1)
    (hxy : dist x y/r ≤ 1) :
    |(∑ s, z s*θ s*f (dist s x/r))-(∑ s, z s*θ s*f (dist s y/r))| ≤
      B*C*(dist x y/r) := by
…

Mentions: OAI.UniformKServer.PilotCompact.gate

theorem OAI.UniformKServer.PilotCompact.integrand_global_lipschitz line 62
theorem OAI.UniformKServer.PilotCompact.radius_sum_le line 125
Source documentation
The geometric bound is valid for an arbitrary finite selection of scales.
```
theorem radius_sum_le (r τ : ℝ) (hr : 0 ≤ r) (hτ : 2 ≤ τ) (n : ℕ) :
    (∑ j ∈ Finset.range (n+1), r*τ^j) ≤ 2*(r*τ^n) := by
…
```
theorem OAI.UniformKServer.PilotCompact.radius_subsum_le line 135

theorem OAI.UniformKServer.PilotCompact.inner_mass_half line 156

Source documentation

Domination by the old measure turns the mover's first moment into an inner-ball mass lower bound, without a cardinality or aspect-ratio loss.

theorem inner_mass_half (r γ : ℝ) (hr : 0 < r) (hγ : 0 < γ)
    (μ ν : X → ℝ) (_hμ : ∀ y, 0 ≤ μ y) (hν : ∀ y, 0 ≤ ν y)
    (hν1 : ∑ y, ν y = 1) (hνμ : ∀ y, ν y ≤ μ y) (x : X)
    (he : 2*(∑ y, ν y*dist x y) ≤ γ*r) :
    1/2 ≤ ballMass r γ μ x := by
…

Mentions: OAI.UniformKServer.PilotCompact.ballMass

theorem OAI.UniformKServer.PilotCompact.drift_nonneg_bound line 176
theorem OAI.UniformKServer.PilotCompact.drift_bounded line 184
theorem OAI.UniformKServer.PilotCompact.drift_lipschitz line 203