Parameters for the Flag Decomposition Lemma

The explicit initial scale ε² / (16 * 3^(d+1)) satisfies the parameter choices in the paper. The geometric estimates include arbitrary tails, so they also control every finite execution of the refinement procedure.

def EGZ.DecompositionParameters.refinementConstant (d : ℕ) : ℝ

The constant in the mass loss of a complete-element refinement.

Equations

• EGZ.DecompositionParameters.refinementConstant d = 3 ^ (d + 1)

noncomputable def EGZ.DecompositionParameters.decayRatio (d : ℕ) : ℝ

The ratio between two consecutive scales.

Equations

• EGZ.DecompositionParameters.decayRatio d = 3⁻¹ ^ (2 * d)

noncomputable def EGZ.DecompositionParameters.scale (d : ℕ) (δ₀ : ℝ) (i : ℕ) : ℝ

The scale δ_i = δ₀ 3^(-2di).

Equations

• EGZ.DecompositionParameters.scale d δ₀ i = δ₀ * EGZ.DecompositionParameters.decayRatio d ^ i

noncomputable def EGZ.DecompositionParameters.lossBudget (d : ℕ) (ε δ₀ : ℝ) (i : ℕ) : ℝ

A bound for the mass lost at one stage, divided by the input mass.

Equations

• EGZ.DecompositionParameters.lossBudget d ε δ₀ i = ε * EGZ.DecompositionParameters.scale d δ₀ i ^ 2 + EGZ.DecompositionParameters.refinementConstant d * EGZ.DecompositionParameters.scale d δ₀ i

noncomputable def EGZ.DecompositionParameters.initialScale (d : ℕ) (ε : ℝ) : ℝ

A choice depending only on the dimension and retained-mass tolerance.

Equations

• EGZ.DecompositionParameters.initialScale d ε = ε ^ 2 / (16 * EGZ.DecompositionParameters.refinementConstant d)

theorem EGZ.DecompositionParameters.refinementConstant_pos (d : ℕ) : 0 < refinementConstant d

theorem EGZ.DecompositionParameters.one_le_refinementConstant (d : ℕ) : 1 ≤ refinementConstant d

theorem EGZ.DecompositionParameters.decayRatio_pos (d : ℕ) : 0 < decayRatio d

theorem EGZ.DecompositionParameters.decayRatio_le_half {d : ℕ} (hd : 1 ≤ d) : decayRatio d ≤ 1 / 2

theorem EGZ.DecompositionParameters.scale_eq_inv_pow (d : ℕ) (δ₀ : ℝ) (i : ℕ) : scale d δ₀ i = δ₀ * 3⁻¹ ^ (2 * d * i)

@[simp]

theorem EGZ.DecompositionParameters.scale_zero (d : ℕ) (δ₀ : ℝ) : scale d δ₀ 0 = δ₀

theorem EGZ.DecompositionParameters.scale_pos (d : ℕ) {δ₀ : ℝ} (hδ : 0 < δ₀) (i : ℕ) : 0 < scale d δ₀ i

theorem EGZ.DecompositionParameters.scale_antitone {d : ℕ} (hd : 1 ≤ d) {δ₀ : ℝ} (hδ : 0 ≤ δ₀) : Antitone (scale d δ₀)

theorem EGZ.DecompositionParameters.scale_le_geometric {d : ℕ} (hd : 1 ≤ d) {δ₀ : ℝ} (hδ : 0 ≤ δ₀) (i : ℕ) : scale d δ₀ i ≤ δ₀ * (1 / 2) ^ i

theorem EGZ.DecompositionParameters.initialScale_pos (d : ℕ) {ε : ℝ} (hε : 0 < ε) : 0 < initialScale d ε

theorem EGZ.DecompositionParameters.refinementConstant_mul_initialScale (d : ℕ) (ε : ℝ) : refinementConstant d * initialScale d ε = ε ^ 2 / 16

theorem EGZ.DecompositionParameters.initialScale_bounds (d : ℕ) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) : refinementConstant d * initialScale d ε < 1 ∧ initialScale d ε ≤ 1 ∧ ε * initialScale d ε ≤ refinementConstant d ∧ initialScale d ε ≤ ε * 3⁻¹ ^ d

Basic inequalities for the explicit initial scale.

theorem EGZ.DecompositionParameters.initialScale_scale_bound {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (i : ℕ) : scale d (initialScale d ε) i ≤ ε * 3⁻¹ ^ d * 2⁻¹ ^ i

theorem EGZ.DecompositionParameters.lossBudget_nonneg (d : ℕ) {ε δ₀ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ₀) (i : ℕ) : 0 ≤ lossBudget d ε δ₀ i

theorem EGZ.DecompositionParameters.lossBudget_le_geometric {d : ℕ} (hd : 1 ≤ d) {ε δ₀ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ₀) (hsmall : ε * δ₀ ≤ refinementConstant d) (i : ℕ) : lossBudget d ε δ₀ i ≤ 2 * refinementConstant d * δ₀ * (1 / 2) ^ i

theorem EGZ.DecompositionParameters.lossBudget_summable {d : ℕ} (hd : 1 ≤ d) {ε δ₀ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ₀) (hsmall : ε * δ₀ ≤ refinementConstant d) : Summable (lossBudget d ε δ₀)

theorem EGZ.DecompositionParameters.lossBudget_tsum_tail_le {d : ℕ} (hd : 1 ≤ d) {ε δ₀ : ℝ} (hε : 0 ≤ ε) (hδ : 0 ≤ δ₀) (hsmall : ε * δ₀ ≤ refinementConstant d) (s : ℕ) : ∑' (i : ℕ), lossBudget d ε δ₀ (i + s + 1) ≤ 2 * refinementConstant d * δ₀ * (1 / 2) ^ s

Every tail of the loss budgets has a geometric bound.

theorem EGZ.DecompositionParameters.initialScale_tsum_tail_le {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (s : ℕ) : ∑' (i : ℕ), lossBudget d ε (initialScale d ε) (i + s + 1) ≤ ε ^ 2 / 8 * 2⁻¹ ^ s

For the chosen scale, the total future budget after stage s is at most ε² / 8 * 2^(-s). In particular, s = 0 is the parameter-choice inequality in the paper.

theorem EGZ.DecompositionParameters.initialScale_summable {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) : Summable (lossBudget d ε (initialScale d ε))

theorem EGZ.DecompositionParameters.initialScale_sum_tail_le {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (s : ℕ) (t : Finset ℕ) : ∑ i ∈ t, lossBudget d ε (initialScale d ε) (i + s + 1) ≤ ε ^ 2 / 8 * 2⁻¹ ^ s

The same bound applies to any finite subset of future stages.

theorem EGZ.DecompositionParameters.exists_parameter_choice {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) : ∃ (δ₀ : ℝ), 0 < δ₀ ∧ refinementConstant d * δ₀ < 1 ∧ (Summable fun (i : ℕ) => lossBudget d ε δ₀ (i + 1)) ∧ ∑' (i : ℕ), lossBudget d ε δ₀ (i + 1) ≤ ε ^ 2 / 8 ∧ ∀ (i : ℕ), scale d δ₀ i ≤ ε * 3⁻¹ ^ d * 2⁻¹ ^ i

All three parameter requirements, with the dependence on d and ε made explicit by the witness initialScale d ε.

theorem EGZ.DecompositionParameters.mass_loss_le {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (mass : ℕ → ℝ) {M : ℝ} (hM : 0 ≤ M) (hstep : ∀ (i : ℕ), mass i - mass (i + 1) ≤ lossBudget d ε (initialScale d ε) (i + 1) * M) (s n : ℕ) : mass s - mass (n + s) ≤ ε ^ 2 / 8 * 2⁻¹ ^ s * M

Telescoping the individual stage estimates gives a bound for every finite interval of an iteration.

theorem EGZ.DecompositionParameters.mass_and_tail {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (mass : ℕ → ℝ) {M : ℝ} (hM : 0 ≤ M) (hmass : mass 0 = M) (hstep : ∀ (i : ℕ), mass i - mass (i + 1) ≤ lossBudget d ε (initialScale d ε) (i + 1) * M) : (∀ (s : ℕ), M / 2 ≤ mass s ∧ (1 - ε) * M ≤ mass s) ∧ ∀ (s n : ℕ), mass s - mass (n + s) ≤ ε ^ 2 / 4 * mass s

The mass-and-tail invariant in the paper, and the final retained-mass bound, follow directly from the explicit budgets. This theorem applies to every finite prefix; an infinite execution is not required.

theorem EGZ.DecompositionParameters.gap_threshold_of_cleanup {d i : ℕ} (hi : 1 ≤ i) {ε δ K N M M' G : ℝ} (hε : 0 ≤ ε) (hK : 1 ≤ K) (hN : 0 < N) (hNcard : N ≤ 2 ^ (i - 1)) (hM : 0 ≤ M) (hretained : M / 2 ≤ M') (hscale : δ ≤ ε * 3⁻¹ ^ d * 2⁻¹ ^ i) (hgap : ε * δ ^ 2 * (2 * K + 1)⁻¹ ^ d * N⁻¹ * M' ≤ G) : δ ^ 3 * K⁻¹ ^ d * M ≤ G

Equation (26): a cleanup at stage i establishes the gap trigger at its own scale. There are at most 2^(i-1) nodes before stage i; the additional factor 1/2 from retained mass gives exactly 2^(-i).

N is the number of old nodes, regarded as a real number. Its strict positivity is needed when taking its reciprocal.

theorem EGZ.DecompositionParameters.initialScale_gap_threshold {d i : ℕ} (hd : 1 ≤ d) (hi : 1 ≤ i) {ε K N M M' G : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (hK : 1 ≤ K) (hN : 0 < N) (hNcard : N ≤ 2 ^ (i - 1)) (hM : 0 ≤ M) (hretained : M / 2 ≤ M') (hgap : ε * scale d (initialScale d ε) i ^ 2 * (2 * K + 1)⁻¹ ^ d * N⁻¹ * M' ≤ G) : scale d (initialScale d ε) i ^ 3 * K⁻¹ ^ d * M ≤ G

The gap-trigger estimate specialized to the explicit parameter choice.