Numerical invariants of finite refinement runs

The state at stage i has at most 2^i nodes, lies within the predetermined radius horizon, and has lost at most the first i explicit mass budgets.

noncomputable def EGZ.FlagDecomposition.Iteration.stageScale (d : ℕ) (ε : ℝ) (i : ℕ) : ℝ

Scale assigned to a given stage of the bounded iteration.

Equations

• EGZ.FlagDecomposition.Iteration.stageScale d ε i = EGZ.DecompositionParameters.scale d (EGZ.DecompositionParameters.initialScale d ε) (i + 1)

noncomputable def EGZ.FlagDecomposition.Iteration.prefixBudget (d : ℕ) (ε : ℝ) (i : ℕ) : ℝ

Accumulated mass-loss budget before a given iteration index.

Equations

• EGZ.FlagDecomposition.Iteration.prefixBudget d ε i = ∑ j ∈ Finset.range i, EGZ.DecompositionParameters.lossBudget d ε (EGZ.DecompositionParameters.initialScale d ε) (j + 1)

@[simp]

theorem EGZ.FlagDecomposition.Iteration.prefixBudget_zero (d : ℕ) (ε : ℝ) : prefixBudget d ε 0 = 0

theorem EGZ.FlagDecomposition.Iteration.prefixBudget_succ (d : ℕ) (ε : ℝ) (i : ℕ) : prefixBudget d ε (i + 1) = prefixBudget d ε i + (ε * stageScale d ε i ^ 2 + 3 ^ (d + 1) * stageScale d ε i)

theorem EGZ.FlagDecomposition.Iteration.prefixBudget_le {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (i : ℕ) : prefixBudget d ε i ≤ ε ^ 2 / 8

theorem EGZ.FlagDecomposition.Iteration.stageScale_pos (d : ℕ) {ε : ℝ} (hε : 0 < ε) (i : ℕ) : 0 < stageScale d ε i

theorem EGZ.FlagDecomposition.Iteration.stageScale_antitone {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) : Antitone (stageScale d ε)

theorem EGZ.FlagDecomposition.Iteration.stageScale_small {d : ℕ} (hd : 1 ≤ d) {ε : ℝ} (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) (i : ℕ) : 3 ^ (d + 1) * stageScale d ε i < 1 ∧ ε * stageScale d ε i ^ 2 < 1

structure EGZ.FlagDecomposition.Iteration.BoundedState {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} (P : NormalizedOperationParameters d g) (ε : ℝ) (i : ℕ) extends EGZ.FlagDecomposition.Iteration.State p d f : Type 1

Iteration state with bounds on node count, radius, and accumulated mass loss.

• decomposition : FlagDecomposition p d f
• radius : ℕ
• radius_pos : 1 ≤ self.radius
• minimal : self.decomposition.IsMinimal
• reduced : self.decomposition.IsReduced
• bounded : self.decomposition.IsKBounded fun (x : self.decomposition.flag.Node) => self.radius
• card_bound : Fintype.card self.decomposition.flag.Node ≤ 2 ^ i
• radius_bound : self.radius ≤ P.radiusHorizon 1 i
• mass_loss_bound : ↑(natMass f) - ↑self.decomposition.retainedMass ≤ prefixBudget d ε i * ↑(natMass f)

theorem EGZ.FlagDecomposition.Iteration.BoundedState.mass_le_input {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) : s.decomposition.retainedMass ≤ natMass f

theorem EGZ.FlagDecomposition.Iteration.BoundedState.mass_bounds {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) (hd : 1 ≤ d) (hε : 0 < ε) (hεhalf : ε ≤ 1 / 2) : ↑(natMass f) / 2 ≤ ↑s.decomposition.retainedMass ∧ (1 - ε) * ↑(natMass f) ≤ ↑s.decomposition.retainedMass

noncomputable def EGZ.FlagDecomposition.Iteration.BoundedState.initial {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} (hf : f ≠ 0) : BoundedState P ε 0

Initial bounded state for a nonzero input weight.

Equations

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

noncomputable def EGZ.FlagDecomposition.Iteration.BoundedState.advance {p d : ℕ} [NeZero p] [Fact (Nat.Prime p)] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) {t : State p d f} (hε : 0 < ε) (D : Progress s.toState t ε (stageScale d ε i) g) (hR : t.radius ≤ P.radiusGrowth s.radius) : BoundedState P ε (i + 1)

Advance a bounded state using a certified progress step and a radius bound.

Equations

• s.advance hε D hR = { toState := t, card_bound := ⋯, radius_bound := ⋯, mass_loss_bound := ⋯ }

noncomputable def EGZ.FlagDecomposition.Iteration.BoundedState.keep {p d : ℕ} [NeZero p] {f : FpCoord p d → ℕ} {g : ℕ → ℕ} {P : NormalizedOperationParameters d g} {ε : ℝ} {i : ℕ} (s : BoundedState P ε i) (hε : 0 < ε) : BoundedState P ε (i + 1)

Retain the same underlying state at the next iteration index.

Equations

• s.keep hε = { toState := s.toState, card_bound := ⋯, radius_bound := ⋯, mass_loss_bound := ⋯ }