The upper approximation bounds the ergodic value

Paper I, the proof of Main Theorem I (2), first half (I:1196–1203): every IRS restricts to a point of the polytope, so the polytope optimum is at least the ergodic value. Here the restriction of an IRS μ to the stage words is a distribution m on patterns; it is carried by locally good patterns, its marginals on the shorter words are conjugation invariant, and it computes the value once the stage covers the challenge words. Rounding m to the grid of step 1/M (exists_rounding, an ℓ¹ error at most 2P) gives a feasible grid point whose value is within 2P/M = 2/2^t of val(T, μ) (valOn_le_upperSeq).

Patterns of sets of words

def MIPRE.Tailored.Sofic.Measure.restrSet (J : List SubgroupTestValue.Word) (q : List Bool) : Set WordSpace

The sets of words with a given pattern on J.

Equations

• MIPRE.Tailored.Sofic.Measure.restrSet J q = {A : MIPRE.Tailored.Sofic.Measure.WordSpace | List.map A J = q}

theorem MIPRE.Tailored.Sofic.Measure.isClopen_restrSet (J : List SubgroupTestValue.Word) (q : List Bool) : IsClopen (restrSet J q)

theorem MIPRE.Tailored.Sofic.Measure.measurableSet_restrSet (J : List SubgroupTestValue.Word) (q : List Bool) : MeasurableSet (restrSet J q)

theorem MIPRE.Tailored.Sofic.Measure.measureReal_partition (ν : MeasureTheory.Measure WordSpace) [MeasureTheory.IsFiniteMeasure ν] (W : List SubgroupTestValue.Word) (Φ : List Bool → Bool) : ν.real {A : WordSpace | Φ (List.map A W) = true} = ∑ p ∈ (allBits W.length).toFinset, if Φ p = true then ν.real (restrSet W p) else 0

The partition by patterns: the measure of a set given by a pattern on W is the sum over the patterns.

Rounding to the grid

theorem MIPRE.Tailored.Sofic.Measure.abs_floor_sub_le {x : ℝ} (hx : 0 ≤ x) : |↑⌊x⌋₊ - x| ≤ 1

theorem MIPRE.Tailored.Sofic.Measure.exists_rounding {α : Type u_1} [DecidableEq α] (F : Finset α) (m : α → ℝ) (hm : ∀ p ∈ F, 0 ≤ m p) (h1 : ∑ p ∈ F, m p = 1) (M : ℕ) : ∃ (nf : α → ℕ), ∑ p ∈ F, nf p = M ∧ (∀ p ∈ F, 0 < nf p → 0 < m p) ∧ ∑ p ∈ F, |↑(nf p) - ↑M * m p| ≤ 2 * ↑F.card

Rounding a distribution to the grid of step 1/M, with ℓ¹ error at most twice the number of points and no new support.

theorem MIPRE.Tailored.Sofic.Measure.sum_ite_key {α : Type u_1} {β : Type u_2} [DecidableEq β] (F : Finset α) (G : Finset β) (key : α → β) (hk : ∀ p ∈ F, key p ∈ G) (c : α → ℝ) : (∑ q ∈ G, ∑ p ∈ F, if key p = q then c p else 0) = ∑ p ∈ F, c p

Summing over the values of a key.

theorem MIPRE.Tailored.Sofic.Measure.sum_abs_cnt_le {α : Type u_1} {β : Type u_2} [DecidableEq β] (F : Finset α) (G : Finset β) (key key' : α → β) (hk : ∀ p ∈ F, key p ∈ G) (hk' : ∀ p ∈ F, key' p ∈ G) (a b : α → ℝ) (hb : ∀ q ∈ G, (∑ p ∈ F, if key p = q then b p else 0) = ∑ p ∈ F, if key' p = q then b p else 0) : ∑ q ∈ G, |(∑ p ∈ F, if key p = q then a p else 0) - ∑ p ∈ F, if key' p = q then a p else 0| ≤ 2 * ∑ p ∈ F, |a p - b p|

The invariance error of a rounding is at most twice its ℓ¹ error.

Lists as finite sums

theorem MIPRE.Tailored.Sofic.Measure.zip_map_self {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : (List.map f l).zip l = List.map (fun (p : α) => (f p, p)) l

theorem MIPRE.Tailored.Sofic.Measure.cntR_map {Pt : List (List Bool)} (hPt : Pt.Nodup) (nf : List Bool → ℕ) (f : List Bool → Bool) : ↑(cntR (List.map nf Pt) Pt f) = ∑ p ∈ Pt.toFinset, if f p = true then ↑(nf p) else 0

The restriction of an IRS

theorem MIPRE.Tailored.Sofic.Measure.mem_stageW (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {u : SubgroupTestValue.Word} : u ∈ stageW T t ↔ List.length u ≤ t + 2 ∧ ∀ l ∈ u, l.1 < T.nGen + t

theorem MIPRE.Tailored.Sofic.Measure.stageD_sub (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {u : SubgroupTestValue.Word} (hu : u ∈ stageD T t) : u ∈ stageW T t

theorem MIPRE.Tailored.Sofic.Measure.conj_mem_stageW (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {g : SubgroupTestValue.Letter} (hg : g.1 < T.nGen) {u : SubgroupTestValue.Word} (hu : u ∈ stageD T t) : invW [g] ++ u ++ [g] ∈ stageW T t

theorem MIPRE.Tailored.Sofic.Measure.stageD_map_extW (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) (A : WordSpace) : List.map (extW (stageW T t) (List.map A (stageW T t))) (stageD T t) = List.map A (stageD T t)

The pattern on the stage of the image of a set of words, on the comparison words.

theorem MIPRE.Tailored.Sofic.Measure.stageD_map_conjW (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {g : SubgroupTestValue.Letter} (hg : g.1 < T.nGen) (A : WordSpace) : List.map (conjW g (extW (stageW T t) (List.map A (stageW T t)))) (stageD T t) = List.map (conjW g A) (stageD T t)

theorem MIPRE.Tailored.Sofic.Measure.list_weighted_bound {α : Type u_1} (l : List α) (w a b : α → ℝ) (E : ℝ) (hw : ∀ x ∈ l, 0 ≤ w x) (h : ∀ x ∈ l, |a x - b x| ≤ E) : (List.map (fun (x : α) => w x * a x) l).sum - E * (List.map w l).sum ≤ (List.map (fun (x : α) => w x * b x) l).sum

A weighted sum of pointwise bounds.

Validity

theorem MIPRE.Tailored.Sofic.Measure.ceilDiv_ge {x D : ℕ} (hD : 0 < D) : ↑x / ↑D ≤ ↑(ceilDiv x D)

theorem MIPRE.Tailored.Sofic.Measure.stagePt_nodup (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : (stagePt T t).Nodup

theorem MIPRE.Tailored.Sofic.Measure.stageP_eq_card (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) : stageP T t = (stagePt T t).toFinset.card

theorem MIPRE.Tailored.Sofic.Measure.exists_feasible_of_irs (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {μ : MeasureTheory.ProbabilityMeasure (SubgroupTestValue.SubgroupSpace T.nGen)} (hμ : μ ∈ SubgroupTestValue.IRS T.nGen) : ∃ n ∈ allVecs (stageP T t) (stageM T t), Feasible T t n ∧ (Covers T t → 0 < T.totalWeight → ↑(stageM T t) * ↑T.totalWeight * T.valOn μ - 2 * ↑(stageP T t) * ↑T.totalWeight ≤ ↑(numG T t n))

The rounding of an IRS: a feasible grid point whose value is within 2P/M of the IRS's once the stage covers the challenge words.

theorem MIPRE.Tailored.Sofic.Measure.valOn_le_upperSeq (T : SubgroupTestValue.SubgroupTestData) (t : ℕ) {μ : MeasureTheory.ProbabilityMeasure (SubgroupTestValue.SubgroupSpace T.nGen)} (hμ : μ ∈ SubgroupTestValue.IRS T.nGen) : T.valOn μ ≤ dyadic (upperSeq T t) t

Every IRS is below the upper approximation.