The upper approximation converges to the ergodic value

Paper I, the proof of Main Theorem I (2), clause (3) (I:1204–1217). A feasible grid point is a probability measure on sets of words (liftMeasure, the distribution n/M on the sets of words of the patterns). For the best feasible grid point at each stage, these measures satisfy the hypotheses of eventually_valΩ_le: a locally good pattern avoids the bad sets within the stage (extW_not_mem_badSet), and the invariance error bounds the change of the measure of a cylinder under conjugation (abs_lift_cyl_sub_le). Their values are within 2/2^t of the polytope optimum, so the upper approximation tends to the ergodic value (tendsto_upperSeq).

Grid points as measures

noncomputable def MIPRE.Tailored.Sofic.Measure.liftMeasure (W : List SubgroupTestValue.Word) (Pt : List (List Bool)) (n : List ℕ) (M : ℕ) : MeasureTheory.Measure WordSpace

The distribution n/M on the sets of words of the patterns Pt on W.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.listSum_dirac_apply (L : List (ℕ × List Bool)) (f : List Bool → WordSpace) {E : Set WordSpace} (hE : MeasurableSet E) : (List.map (fun (x : ℕ × List Bool) => ↑x.1 • MeasureTheory.Measure.dirac (f x.2)) L).sum E = ↑(List.map (fun (x : ℕ × List Bool) => if decide (f x.2 ∈ E) = true then x.1 else 0) L).sum

theorem MIPRE.Tailored.Sofic.Measure.liftMeasure_apply (W : List SubgroupTestValue.Word) (Pt : List (List Bool)) (n : List ℕ) (M : ℕ) {E : Set WordSpace} (hE : MeasurableSet E) : (liftMeasure W Pt n M) E = (↑M)⁻¹ * ↑(cntR n Pt fun (p : List Bool) => decide (extW W p ∈ E))

theorem MIPRE.Tailored.Sofic.Measure.liftMeasure_real (W : List SubgroupTestValue.Word) (Pt : List (List Bool)) (n : List ℕ) (M : ℕ) {E : Set WordSpace} (hE : MeasurableSet E) : (liftMeasure W Pt n M).real E = ↑(cntR n Pt fun (p : List Bool) => decide (extW W p ∈ E)) / ↑M

theorem MIPRE.Tailored.Sofic.Measure.cntR_true {n : List ℕ} {Pt : List (List Bool)} (h : n.length ≤ Pt.length) : (cntR n Pt fun (x : List Bool) => true) = n.sum

theorem MIPRE.Tailored.Sofic.Measure.isProbabilityMeasure_liftMeasure (W : List SubgroupTestValue.Word) {Pt : List (List Bool)} {n : List ℕ} {M : ℕ} (hM : 0 < M) (hlen : n.length ≤ Pt.length) (hsum : n.sum = M) : MeasureTheory.IsProbabilityMeasure (liftMeasure W Pt n M)

The cylinders under conjugation

theorem MIPRE.Tailored.Sofic.Measure.list_abs_sum_le {α : Type u_1} (l : List α) (f : α → ℝ) : |(List.map f l).sum| ≤ (List.map (fun (x : α) => |f x|) l).sum

theorem MIPRE.Tailored.Sofic.Measure.list_sum_map_sub {α : Type u_1} (l : List α) (f g : α → ℝ) : (List.map (fun (x : α) => f x - g x) l).sum = (List.map f l).sum - (List.map g l).sum

theorem MIPRE.Tailored.Sofic.Measure.sum_single {α : Type u_1} [DecidableEq α] {Q : List α} (hQ : Q.Nodup) {a : α} (ha : a ∈ Q) (g : α → ℝ) : (List.map (fun (q : α) => if a = q then g q else 0) Q).sum = g a

theorem MIPRE.Tailored.Sofic.Measure.list_sum_comm {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) (f : α → β → ℝ) : (List.map (fun (a : α) => (List.map (fun (b : β) => f a b) l₂).sum) l₁).sum = (List.map (fun (b : β) => (List.map (fun (a : α) => f a b) l₁).sum) l₂).sum

theorem MIPRE.Tailored.Sofic.Measure.cntR_comp_key (n : List ℕ) (Pt : List (List Bool)) {Q : List (List Bool)} (hQ : Q.Nodup) (key : List Bool → List Bool) (hk : ∀ (p : List Bool), key p ∈ Q) (c : List Bool → Bool) : ↑(cntR n Pt fun (p : List Bool) => c (key p)) = (List.map (fun (q : List Bool) => if c q = true then ↑(cntR n Pt fun (p : List Bool) => key p == q) else 0) Q).sum

theorem MIPRE.Tailored.Sofic.Measure.abs_lift_cyl_sub_le (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) (n : List ℕ) (g : SubgroupTestValue.Letter) {J : List SubgroupTestValue.Word} (hJ : ∀ u ∈ J, u ∈ stageD T t) (q₀ : List Bool) : |(liftMeasure (stageW T t) (stagePt T t) n (stageM T t)).real (restrSet J q₀) - (liftMeasure (stageW T t) (stagePt T t) n (stageM T t)).real (conjW g ⁻¹' restrSet J q₀)| ≤ ↑(invErr T t g n) / ↑(stageM T t)

The change of a cylinder under conjugation, for the distribution of a grid point: at most the invariance error over M.

noncomputable def MIPRE.Tailored.Sofic.Measure.liftStage (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) (n : List ℕ) (hn : n ∈ allVecs (stageP T t) (stageM T t)) (hf : Feasible T t n) : MeasureTheory.ProbabilityMeasure WordSpace

The distribution of a feasible grid point is a probability measure.

Equations

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

theorem MIPRE.Tailored.Sofic.Measure.valΩ_liftStage (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) (n : List ℕ) (hn : n ∈ allVecs (stageP T t) (stageM T t)) (hf : Feasible T t n) : valΩ T (liftStage T t n hn hf) = ↑(numG T t n) / (↑(stageM T t) * ↑T.totalWeight)

theorem MIPRE.Tailored.Sofic.Measure.lift_badSet (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) (n : List ℕ) (hn : n ∈ allVecs (stageP T t) (stageM T t)) (hf : Feasible T t n) (b : Unit ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word ⊕ SubgroupTestValue.Word × SubgroupTestValue.Word × ℕ × Bool) (hb : ∀ w ∈ badWords b, w ∈ stageW T t) : ↑(liftStage T t n hn hf) (badSet T.nGen b) = 0

Eventually in the stage

theorem MIPRE.Tailored.Sofic.Measure.eventually_mem_stageD (T : SubgroupTestValue.SubgroupTestData) (w : SubgroupTestValue.Word) : ∀ᶠ (t : ℕ) in Filter.atTop, w ∈ stageD T t

theorem MIPRE.Tailored.Sofic.Measure.eventually_forall_mem_stageD (T : SubgroupTestValue.SubgroupTestData) (L : List SubgroupTestValue.Word) : ∀ᶠ (t : ℕ) in Filter.atTop, ∀ w ∈ L, w ∈ stageD T t

theorem MIPRE.Tailored.Sofic.Measure.eventually_forall_mem_stageW (T : SubgroupTestValue.SubgroupTestData) (L : List SubgroupTestValue.Word) : ∀ᶠ (t : ℕ) in Filter.atTop, ∀ w ∈ L, w ∈ stageW T t

theorem MIPRE.Tailored.Sofic.Measure.eventually_covers (T : SubgroupTestValue.SubgroupTestData) : ∀ᶠ (t : ℕ) in Filter.atTop, Covers T t

theorem MIPRE.Tailored.Sofic.Measure.eventually_div_pow_le (c : ℝ) {η : ℝ} (hη : 0 < η) : ∀ᶠ (t : ℕ) in Filter.atTop, c / 2 ^ t ≤ η

Convergence

theorem MIPRE.Tailored.Sofic.Measure.exists_max_feasible (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : ∃ (n : List ℕ) (_ : n ∈ allVecs (stageP T t) (stageM T t)), Feasible T t n ∧ maxNum T t ≤ numG T t n

theorem MIPRE.Tailored.Sofic.Measure.valErg_eq_zero (T : SubgroupTestValue.SubgroupTestData) (hW : T.totalWeight = 0) : T.valErg = 0

theorem MIPRE.Tailored.Sofic.Measure.valErg_le_upperSeq (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : T.valErg ≤ dyadic (upperSeq T t) t

theorem MIPRE.Tailored.Sofic.Measure.dyadic_ceilDiv_le {X D : ℕ} (t : ℕ) (hD : 0 < D) : dyadic (ceilDiv (2 ^ t * X) D) t ≤ ↑X / ↑D + 1 / 2 ^ t

The rounding up in upperSeq.

theorem MIPRE.Tailored.Sofic.Measure.tendsto_upperSeq (T : SubgroupTestValue.SubgroupTestData) : Filter.Tendsto (fun (t : ℕ) => dyadic (upperSeq T t) t) Filter.atTop (nhds T.valErg)

The upper approximation tends to the ergodic value (Main Theorem I (2), clause (3) of its proof).