structure ProjectionTheory.DoubleCountingRealHausdorffSetupextends ProjectionTheory.DoubleCountingRealSetup : Type

A DoubleCountingRealSetup augmented with the Hausdorff (a.k.a. dimension) spacing hypotheses on both X and D: the covering numbers obey N_X(R^β) ≲ |X|^β and N_D(R^{β-1}) ≲ |D|^β for every β ∈ [0, 1].

• R : ℝ
• hR : 1 ≤ self.R
• cardX : ℕ
• cardD : ℕ
• S : ℕ
• hS_pos : 0 < self.S
• hS_le : self.S ≤ self.cardX
• N_X : ℝ → ℕ
• N_D : ℝ → ℕ
• hN_X_le (r : ℝ) : self.N_X r ≤ self.cardX
• hN_D_le (ρ : ℝ) : self.N_D ρ ≤ self.cardD
• C_X : ℝ
• hC_X_pos : 0 < self.C_X
• hHausdorff_X (β : ℝ) : 0 ≤ β → β ≤ 1 → ↑(self.N_X (self.R ^ β)) ≤ self.C_X * ↑self.cardX ^ β
• C_D : ℝ
• hC_D_pos : 0 < self.C_D
• hHausdorff_D (β : ℝ) : 0 ≤ β → β ≤ 1 → ↑(self.N_D (self.R ^ (β - 1))) ≤ self.C_D * ↑self.cardD ^ β

theorem ProjectionTheory.double_counting_real_hausdorff_dichotomy_line683 (setup : DoubleCountingRealHausdorffSetup) (hX_pos : 0 < setup.cardX) (hD_pos : 0 < setup.cardD) (hR_gt : 1 < setup.R) (h_intermediate : ∃ C > 0, ↑setup.cardD ≤ C * Real.log setup.R * (↑setup.S + ↑setup.S * ↑setup.cardD / ↑setup.cardX)) : ∃ C > 0, ↑setup.S ≥ ↑setup.cardX / (C * Real.log setup.R) ∨ ↑setup.cardD ≤ C * Real.log setup.R * ↑setup.S

Corollary (Double Counting Real Version — dichotomy step). Starting from the intermediate bound |D| ≲ log R · (S + S|D|/|X|) produced by the real double-counting theorem combined with Hausdorff spacing, conclude the dichotomy S ≳ |X|/log R or |D| ≲ log R · S.

theorem ProjectionTheory.double_counting_real_hausdorff_dichotomy (setup : DoubleCountingRealHausdorffSetup) (hX_pos : 0 < setup.cardX) (hD_pos : 0 < setup.cardD) (hR_gt : 1 < setup.R) : ∃ C > 0, ↑setup.cardD ≤ C * ↑setup.S * setup.R / ↑setup.cardX

Corollary (Real SETUP with Hausdorff spacing). Under the ℝ-SETUP where both X and D have Hausdorff spacing, |D| ≲ S · R / |X|.