structure ProjectionTheory.ADConfigSpace : Type 1

The abstract data of an AD-regular configuration space at every scale $\delta$: each $\delta$ has a type of configurations whose "ratio" measures the incidence count; configurations at scale $\delta_1 \delta_2$ can be coarsened to scale $\delta_1$ and restricted to scale $\delta_2$, and the ratio factors (up to a sub-polynomial loss) as $R(\delta_1\delta_2) \lessapprox (\delta_1\delta_2)^{-\varepsilon} R(\delta_1) R(\delta_2)$.

• Config : ℝ → Type
• ratio (δ : ℝ) : self.Config δ → ℝ
• ratio_nonneg (δ : ℝ) (c : self.Config δ) : 0 ≤ self.ratio δ c
• ratio_bddAbove (δ : ℝ) : BddAbove (Set.range (self.ratio δ))
• config_nonempty (δ : ℝ) : Nonempty (self.Config δ)
• coarsen (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₁
• restrict (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₂
• ratio_factoring (δ₁ δ₂ : ℝ) (hδ₁ : 0 < δ₁) (hδ₁' : δ₁ < 1) (hδ₂ : 0 < δ₂) (hδ₂' : δ₂ < 1) (ε : ℝ) : 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (c : self.Config (δ₁ * δ₂)), self.ratio (δ₁ * δ₂) c ≤ C * (δ₁ * δ₂)⁻¹ ^ ε * (self.ratio δ₁ (self.coarsen δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c) * self.ratio δ₂ (self.restrict δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c))

structure ProjectionTheory.ADConfigData : Type 1

The raw data of an AD-regular configuration space, equipped only with the pointwise incidence decomposition $R(\delta_1\delta_2) \le R(\delta_1) R(\delta_2)$ (without the $\varepsilon$-loss factor).

• Config : ℝ → Type
• ratio (δ : ℝ) : self.Config δ → ℝ
• ratio_nonneg (δ : ℝ) (c : self.Config δ) : 0 ≤ self.ratio δ c
• ratio_bddAbove (δ : ℝ) : BddAbove (Set.range (self.ratio δ))
• config_nonempty (δ : ℝ) : Nonempty (self.Config δ)
• coarsen (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₁
• restrict (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₂
• incidence_decomp (δ₁ δ₂ : ℝ) (hδ₁ : 0 < δ₁) (hδ₁' : δ₁ < 1) (hδ₂ : 0 < δ₂) (hδ₂' : δ₂ < 1) (c : self.Config (δ₁ * δ₂)) : self.ratio (δ₁ * δ₂) c ≤ self.ratio δ₁ (self.coarsen δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c) * self.ratio δ₂ (self.restrict δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c)

noncomputable def ProjectionTheory.adConfigData : ADConfigData

The concrete AD configuration data used in the projection theory framework.

theorem ProjectionTheory.ratio_factoring_axiom (δ₁ δ₂ : ℝ) (hδ₁ : 0 < δ₁) (hδ₁' : δ₁ < 1) (hδ₂ : 0 < δ₂) (hδ₂' : δ₂ < 1) (ε : ℝ) : 0 < ε → ∃ (C : ℝ), 0 < C ∧ ∀ (c : adConfigData.Config (δ₁ * δ₂)), adConfigData.ratio (δ₁ * δ₂) c ≤ C * (δ₁ * δ₂)⁻¹ ^ ε * (adConfigData.ratio δ₁ (adConfigData.coarsen δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c) * adConfigData.ratio δ₂ (adConfigData.restrict δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c))

Derivation of the $\varepsilon$-loss factoring axiom for adConfigData from its pointwise incidence decomposition: the ratio at scale $\delta_1\delta_2$ is bounded by $C \cdot (\delta_1\delta_2)^{-\varepsilon}$ times the product of ratios at scales $\delta_1$ and $\delta_2$.

noncomputable def ProjectionTheory.adConfigSpace : ADConfigSpace

The AD configuration space obtained from adConfigData by promoting its pointwise incidence decomposition to the submultiplicative factoring axiom.

noncomputable def ProjectionTheory.R_AD (δ : ℝ) : ℝ

The AD-regular incidence quantity $R_{AD}(\delta)$ at scale $\delta$, defined as the supremum of the configuration ratios over all configurations at scale $\delta$.

theorem ProjectionTheory.R_AD_nonneg (δ : ℝ) : 0 ≤ R_AD δ

$R_{AD}(\delta) \ge 0$ for every scale $\delta$.

theorem ProjectionTheory.ratio_le_R_AD (δ : ℝ) (c : adConfigSpace.Config δ) : adConfigSpace.ratio δ c ≤ R_AD δ

Each individual configuration ratio is bounded by the supremum $R_{AD}(\delta)$.

theorem ProjectionTheory.R_AD_submultiplicative (δ₁ δ₂ : ℝ) (hδ₁ : 0 < δ₁) (hδ₁' : δ₁ < 1) (hδ₂ : 0 < δ₂) (hδ₂' : δ₂ < 1) (ε : ℝ) : 0 < ε → ∃ (C : ℝ), 0 < C ∧ R_AD (δ₁ * δ₂) ≤ C * (δ₁ * δ₂)⁻¹ ^ ε * (R_AD δ₁ * R_AD δ₂)

Submultiplicative Lemma. If $\delta = \delta_1 \delta_2$ with $\delta_1, \delta_2 < 1$, then for every $\varepsilon > 0$ there is a constant $C > 0$ such that $R_{AD}(\delta_1\delta_2) \le C \cdot (\delta_1\delta_2)^{-\varepsilon} \cdot R_{AD}(\delta_1) \cdot R_{AD}(\delta_2)$, i.e. $R_{AD}$ is submultiplicative up to a sub-polynomial loss.