AdmissibleListCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Choose a longest top and count the remaining directions against it.

theorem OAI.LipschitzHilbert.SlopeBox.admissible_list_card_le line 16

Source documentation

The reference top contributes one; all other tops inject into popular angular bins for the longest top. All reference counts are chosen in advance.

theorem admissible_list_card_le {ι : Type*} [DecidableEq ι]
    (T : ι → SlopeBox) (I : Finset ι) (u : ℝ × ℝ → ℝ)
    {L : ℝ≥0} (hu : LipschitzWith L u) (z : ℝ × ℝ)
    {M : ℕ} (hM : 0 < M) {A q P K θ c c0 B rho m lambda : ℝ}
    (hA : 0 < A) (hq : 0 < q) (hP : 0 < P) (hK : 0 ≤ K)
    (hAK : A + K ≤ P) (hc0 : 0 ≤ c0) (hc : 4 * (c0 + 1) + 1 ≤ c)
    (hB : 1 < B) (hrho : 0 < rho) (hMB : (M : ℝ) = B ^ 2) (hm : B ^ 2 ≤ m)
    (hθ : θ ≤ q / (8 * A * P)) (hlambda : 0 ≤ lambda)
    (d : ι → ℝ) (E : ι → Set (ℝ × ℝ))
    (hE : ∀ i ∈ I, MeasurableSet (E i))
    (hfinite : ∀ i ∈ I, (volume.prod volume) (E i) ≠ ∞)
    (hbox : ∀ i ∈ I, ∀ w ∈ E i, (T i).radius w ≤ A)
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.SlopeBox.radius