Progress certificates for face and complete-element refinements #
The concrete normalized operations satisfy the iteration's level, stable mass transport, parent injectivity, resolution, and numerical requirements.
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.Iteration.faceState
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{anchor : s.decomposition.flag.Node}
{Γ : (s.decomposition.flag.polytope anchor).Face}
(D : NormalizedFaceStep s.decomposition anchor Γ s.radius R)
:
State p d f
The iteration state produced by a normalized face refinement step.
Equations
- EGZ.FlagDecomposition.Iteration.faceState s D = { decomposition := D.decomposition, radius := D.radius, radius_pos := ⋯, minimal := ⋯, reduced := ⋯, bounded := ⋯ }
Instances For
@[reducible, inline]
noncomputable abbrev
EGZ.FlagDecomposition.Iteration.completeState
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{anchor : s.decomposition.flag.Node}
{g : ℕ → ℕ}
{δ : ℝ}
{hδ : 0 ≤ δ}
{hsmall : 3 ^ (d + 1) * δ < 1}
(D : NormalizedCompleteStep s.decomposition anchor g s.radius R δ hδ hsmall)
:
State p d f
The iteration state produced by a normalized completion step.
Equations
- EGZ.FlagDecomposition.Iteration.completeState s D = { decomposition := D.decomposition, radius := D.radius, radius_pos := ⋯, minimal := ⋯, reduced := ⋯, bounded := ⋯ }
Instances For
noncomputable def
EGZ.FlagDecomposition.Iteration.faceProgress
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{anchor : s.decomposition.flag.Node}
{Γ : (s.decomposition.flag.polytope anchor).Face}
{ε δ : ℝ}
{g : ℕ → ℕ}
(D : NormalizedFaceStep s.decomposition anchor Γ s.radius R)
(hvalid : State.Event.Valid ε δ g (State.Event.face anchor Γ))
(hε : 0 ≤ ε)
(hδ : 0 ≤ δ)
:
A valid face event supplies every field of a progress certificate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EGZ.FlagDecomposition.Iteration.completeStep_count_pos
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{anchor : s.decomposition.flag.Node}
{ε δ : ℝ}
{g : ℕ → ℕ}
{hδ : 0 ≤ δ}
{hsmall : 3 ^ (d + 1) * δ < 1}
(D : NormalizedCompleteStep s.decomposition anchor g s.radius R δ hδ hsmall)
(hvalid : State.Event.Valid ε δ g (State.Event.complete anchor))
(hg : Monotone g)
:
A valid incomplete-element event forces a positive number of added directions, even though the actual output radius is chosen with the charts.
noncomputable def
EGZ.FlagDecomposition.Iteration.completeProgress
{p d : ℕ}
[NeZero p]
[Fact (Nat.Prime p)]
{f : FpCoord p d → ℕ}
(s : State p d f)
{R : ℕ}
{anchor : s.decomposition.flag.Node}
{ε δ : ℝ}
{g : ℕ → ℕ}
{hδ : 0 ≤ δ}
{hsmall : 3 ^ (d + 1) * δ < 1}
(D : NormalizedCompleteStep s.decomposition anchor g s.radius R δ hδ hsmall)
(hvalid : State.Event.Valid ε δ g (State.Event.complete anchor))
(hε : 0 ≤ ε)
(hg : Monotone g)
:
Progress s (completeState s D) ε δ g
The complete-element construction supplies stable mass maps at all nodes and removes every low-level child of the selected anchor.
Equations
- One or more equations did not get rendered due to their size.