Uniform balanced coefficients at the selected flag node

The fraction and length threshold are functions of the coordinate radius chosen before the driving function, decomposition, prime, or selected node. The normalized input and gap estimates place the selected cumulative weight within their scope. The centrality identity then gives the reserve required by relative expansion.

def EGZ.MainProof.RoundingBound (d K : ℕ) (C γ η μ : ℝ) (N : ℕ) : Prop

The bounded-rounding conclusion for one prescribed coordinate radius.

Equations

• One or more equations did not get rendered due to their size.

structure EGZ.MainProof.CoefficientParameters (d : ℕ) (δ ζ : ℝ) : Type

The radius-dependent parameters used before choosing the flag lemma's driving function. Radius zero receives harmless positive default data.

• fraction : ℕ → ℝ

  The positive retained fraction used in the rounding bound at each radius.

• threshold : ℕ → ℕ

  The size threshold required for the rounding bound at each radius.

• fraction_pos (K : ℕ) : 0 < self.fraction K
• bound (K : ℕ) : 1 ≤ K → RoundingBound d K (↑(hollowBound d) + 2) (gapScale d δ K) (errorScale (↑(hollowBound d)) ζ) (self.fraction K) (self.threshold K)

theorem EGZ.MainProof.exists_coefficientParameters (hBalanced : BalancedCombinationLemma) (d : ℕ) {δ ζ : ℝ} (hδ : 0 < δ) (hζ : 0 < ζ) (hζone : ζ ≤ 1) : Nonempty (CoefficientParameters d δ ζ)

noncomputable def EGZ.MainProof.coefficientParameters (hBalanced : BalancedCombinationLemma) (d : ℕ) {δ ζ : ℝ} (hδ : 0 < δ) (hζ : 0 < ζ) (hζone : ζ ≤ 1) : CoefficientParameters d δ ζ

Choose radius-dependent rounding parameters from the balanced combination lemma.

Equations

• EGZ.MainProof.coefficientParameters hBalanced d hδ hζ hζone = Classical.choice ⋯

noncomputable def EGZ.MainProof.CoefficientParameters.expansionScale {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) (K : ℕ) : ℝ

A common scale for thickness and the reserve on both sides of each coefficient. It is fixed as a function of the old radius before the flag decomposition's driving function is chosen.

Equations

• P.expansionScale K = min (P.fraction K) (min δ (EGZ.MainProof.errorScale (↑(EGZ.MainProof.hollowBound d)) ζ * EGZ.MainProof.gapScale d δ K))

theorem EGZ.MainProof.CoefficientParameters.expansionScale_pos {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) {K : ℕ} (hδ : 0 < δ) (hζ : 0 < ζ) (hK : 1 ≤ K) : 0 < P.expansionScale K

theorem EGZ.MainProof.CoefficientParameters.expansionScale_le_delta {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) (K : ℕ) : P.expansionScale K ≤ δ

theorem EGZ.MainProof.CoefficientParameters.expansionScale_le_fraction {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) (K : ℕ) : P.expansionScale K ≤ P.fraction K

theorem EGZ.MainProof.CoefficientParameters.expansion_slack {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) {I : Type u_1} (K p : ℕ) (m a : I → ℕ) (hζ : 0 < ζ) (hmlower : ∀ (q : I), gapScale d δ K * ↑p ≤ ↑(m q)) (hlower : ∀ (q : I), P.fraction K * ↑p ≤ ↑(a q)) (hupper : ∀ (q : I), ↑(a q) ≤ (1 - errorScale (↑(hollowBound d)) ζ) * ↑(m q)) (q : I) : P.expansionScale K * ↑p ≤ ↑(a q) ∧ ↑(a q) ≤ ↑(m q) - P.expansionScale K * ↑p

The proportional reserve gives the two additive margins in the relative expansion theorem.

theorem EGZ.MainProof.CoefficientParameters.coefficients_of_selection {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) {p : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {T K : Φ.flag.Node → ℕ} (D : Φ.CumulativeSelection T K δ) (hodd : Odd p) (hδ : 0 < δ) (hζ : 0 < ζ) (hζone : ζ ≤ 1) (hW : ↑(hollowConstant p d) ≤ ↑(hollowBound d)) (hK : 1 ≤ K D.node) (hp : P.threshold (K D.node) < p) (hinput_lower : p ≤ natMass f) (hinput_upper : ↑(natMass f) ≤ (↑(hollowBound d) + 2) * ↑p) (hretained : (1 - errorScale (↑(hollowBound d)) ζ) * (↑(hollowConstant p d) + ζ) * ↑p ≤ ↑Φ.retainedMass) (hgap : ∀ (x : Φ.flag.Node), gapScale d δ (K x) * ↑(natMass f) ≤ ↑(Φ.gap x)) : ∃ (a : ↥(Φ.liftedSupport D.node) → ℕ), ∑ q : ↥(Φ.liftedSupport D.node), a q = p ∧ ∑ q : ↥(Φ.liftedSupport D.node), a q • ↑q = p • D.center ∧ (∀ (q : ↥(Φ.liftedSupport D.node)), P.fraction (K D.node) * ↑p ≤ ↑(a q)) ∧ ∀ (q : ↥(Φ.liftedSupport D.node)), ↑(a q) ≤ (1 - errorScale (↑(hollowBound d)) ζ) * ↑(Φ.hat D.node ↑q)

Apply the parameters to any selected cumulative node. The selection already records that this node is complete at T(node), δ.

theorem EGZ.MainProof.CoefficientParameters.exists_selected_coefficients {d : ℕ} {δ ζ : ℝ} (P : CoefficientParameters d δ ζ) {p : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} (Φ : FlagDecomposition p d f) {T K : Φ.flag.Node → ℕ} (hodd : Odd p) (hδ : 0 < δ) (hζ : 0 < ζ) (hζone : ζ ≤ 1) (hW : ↑(hollowConstant p d) ≤ ↑(hollowBound d)) (hK : ∀ (x : Φ.flag.Node), 1 ≤ K x) (hp : ∀ (x : Φ.flag.Node), P.threshold (K x) < p) (hcomplete : Φ.IsComplete T (errorScale (↑(hollowBound d)) ζ) δ) (hbounded : Φ.IsKBounded K) (hinput_lower : p ≤ natMass f) (hinput_upper : ↑(natMass f) ≤ (↑(hollowBound d) + 2) * ↑p) (hretained : (1 - errorScale (↑(hollowBound d)) ζ) * (↑(hollowConstant p d) + ζ) * ↑p ≤ ↑Φ.retainedMass) (hgap : ∀ (x : Φ.flag.Node), gapScale d δ (K x) * ↑(natMass f) ≤ ↑(Φ.gap x)) : ∃ (D : Φ.CumulativeSelection T K δ) (a : ↥(Φ.liftedSupport D.node) → ℕ), ∑ q : ↥(Φ.liftedSupport D.node), a q = p ∧ ∑ q : ↥(Φ.liftedSupport D.node), a q • ↑q = p • D.center ∧ (∀ (q : ↥(Φ.liftedSupport D.node)), P.fraction (K D.node) * ↑p ≤ ↑(a q)) ∧ ∀ (q : ↥(Φ.liftedSupport D.node)), ↑(a q) ≤ (1 - errorScale (↑(hollowBound d)) ζ) * ↑(Φ.hat D.node ↑q)

A threshold imposed on every allowed node radius permits selecting the node only after the flag decomposition has been constructed.