Gap cleanup as a certified iteration step #
noncomputable def
EGZ.FlagDecomposition.Iteration.gapState
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{ε δ : ℝ}
(D : NormalizedGapStep s.decomposition s.radius R (ε * δ ^ 2))
:
State p d f
Iteration state produced by the gap-cleanup data.
Equations
- EGZ.FlagDecomposition.Iteration.gapState s D = { decomposition := D.decomposition, radius := D.radius, radius_pos := ⋯, minimal := ⋯, reduced := ⋯, bounded := ⋯ }
Instances For
theorem
EGZ.FlagDecomposition.Iteration.gapState_gapCondition
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{ε δ : ℝ}
(D : NormalizedGapStep s.decomposition s.radius R (ε * δ ^ 2))
{i : ℕ}
(hi : 1 ≤ i)
(hε : 0 ≤ ε)
(hcard : Fintype.card s.decomposition.flag.Node ≤ 2 ^ (i - 1))
(hretained : ↑(natMass f) / 2 ≤ ↑s.decomposition.retainedMass)
(hscale : δ ≤ ε * 3⁻¹ ^ d * 2⁻¹ ^ i)
:
(gapState s D).GapCondition δ
noncomputable def
EGZ.FlagDecomposition.Iteration.gapProgress
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{ε δ : ℝ}
(D : NormalizedGapStep s.decomposition s.radius R (ε * δ ^ 2))
(hδ : 0 ≤ δ)
(hvalid : ¬s.GapCondition δ)
(hgap : (gapState s D).GapCondition δ)
(g : ℕ → ℕ)
:
Certify progress of a gap cleanup that restores the gap condition.
Equations
- One or more equations did not get rendered due to their size.