OAI/Analysis/LipschitzHilbert/Estimates/SeparatedWitnessCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SlopeBox.separated_witness_list_count line 17

   Source documentation

   Extract compact witnesses, transfer them to the reference line, and assign distinct angular bins. The reference count is fixed before the list.

   theorem separated_witness_list_count {ι : Type*} [Fintype ι] [DecidableEq ι]
       (R : SlopeBox) (T : ι → SlopeBox) (u : ℝ × ℝ → ℝ)
       {L : ℝ≥0} (hu : LipschitzWith L u) (z : ℝ × ℝ)
       {M : ℕ} (hM : 0 < M) {A q P K θ c c0 B rho m : ℝ}
       (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))
       (d : ι → ℝ) (E : ι → Set (ℝ × ℝ))
       (hE : ∀ i, MeasurableSet (E i))
       (hfinite : ∀ i, (volume.prod volume) (E i) ≠ ∞)
       (hbox : ∀ i, ∀ w ∈ E i, (T i).radius w ≤ A)
   …

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