structure FurstenbergCorollary.RealProjectionSetup : Type

The "real SETUP" data for Euclidean projection theorems: a scale $R > 1$, a point set of cardinality X_card, a direction set of cardinality D_card, a bound S on $\max_{\theta\in D}|\pi_\theta(X)|$, and covering-number functions $N_X(r)$ and $N_D(\rho)$ counting balls of various radii intersecting $X$ and $D$.

• R : ℝ
• hR : 1 < self.R
• X_card : ℕ
• hX_pos : 0 < self.X_card
• D_card : ℕ
• hD_pos : 0 < self.D_card
• S : ℕ
• hS_pos : 0 < self.S
• N_X : ℝ → ℕ
• N_D : ℝ → ℕ

structure FurstenbergCorollary.HasHausdorffSpacing (setup : RealProjectionSetup) : Type

Witness that the sets $X$ and $D$ in a RealProjectionSetup have Hausdorff spacing: there exist exponents $\alpha, \beta \in [0,1]$ and a constant $C$ such that $|X| \sim R^\alpha$, $|D| \sim R^\beta$, $N_X(r) \lesssim r^\alpha$ for all $1 \le r \le R$, and $N_D(\rho) \lesssim (\rho R)^\beta$ for all $R^{-1} \le \rho \le 1$.

• α : ℝ
• hα_nonneg : 0 ≤ self.α
• hα_le_one : self.α ≤ 1
• β : ℝ
• hβ_nonneg : 0 ≤ self.β
• hβ_le_one : self.β ≤ 1
• C : ℝ
• hC_pos : 0 < self.C
• hX_size_lower : self.C⁻¹ * setup.R ^ self.α ≤ ↑setup.X_card
• hX_size_upper : ↑setup.X_card ≤ self.C * setup.R ^ self.α
• hD_size_lower : self.C⁻¹ * setup.R ^ self.β ≤ ↑setup.D_card
• hD_size_upper : ↑setup.D_card ≤ self.C * setup.R ^ self.β
• hN_X_bound (r : ℝ) : 1 ≤ r → r ≤ setup.R → ↑(setup.N_X r) ≤ self.C * r ^ self.α
• hN_D_bound (ρ : ℝ) : setup.R⁻¹ ≤ ρ → ρ ≤ 1 → ↑(setup.N_D ρ) ≤ self.C * (ρ * setup.R) ^ self.β

theorem FurstenbergCorollary.furstenberg_corollary (setup : RealProjectionSetup) (hspacing : HasHausdorffSpacing setup) (ε : ℝ) (hε_pos : 0 < ε) (hS_bound : ↑setup.S ≤ setup.R ^ (-ε) * min setup.R ↑setup.X_card) : ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ ↑setup.D_card ≤ C * setup.R ^ (c * ε) * ↑setup.S ^ 2 / setup.R

Furstenberg conjecture (Euclidean form). In the SETUP, if $X$ and $D$ have Hausdorff spacing and $S \le R^{-\varepsilon}\min(R, |X|)$, then $|D| \lessapprox |S|^2 / R$, i.e. there exist constants $C, c > 0$ with $|D| \le C \cdot R^{c\varepsilon} \cdot S^2 / R$.