OAI/Analysis/LipschitzHilbert/Estimates/SimultaneousCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.simultaneous_separated_count line 18

   Source documentation

   Quantitative simultaneous counting from the original measurable popularity witnesses. The exceptional set is chosen before the point, separation scale, and list, and costs only total top area.

   theorem simultaneous_separated_count {ι : Type*} [Fintype ι] [DecidableEq ι]
       (T : ι → SlopeBox) (u : ℝ × ℝ → ℝ) {L : ℝ≥0} (hu : LipschitzWith L u)
       {M : ℕ} (hM : 0 < M) {A q P K θ c c0 B 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)
       (hcM : c ≤ M) (hB : 1 < B) (hMB : (M : ℝ) = B ^ 2) (hm : B ^ 2 ≤ m)
       (hθ0 : 0 < θ) (hθ : θ ≤ q / (8 * A * P)) (hlambda : 0 ≤ lambda)
       (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)
       (harea : ∀ i, q * (T i).length * (T i).width ≤ (volume.prod volume).real (E i))
   …

   Mentions: OAI.LipschitzHilbert.SlopeBox