WordStep.lean`

62 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SmoothObstruction.ShiftComparisons.first line 15
Source documentation
The exact first endpoint of a comparison against a length-N window in uv. It also includes aligned different-word comparisons when t=0.
```
def first {M N : ℕ} (a b : Fin M) (t r : Fin N) : Fin M × Fin N :=
…
```
def OAI.SmoothObstruction.ShiftComparisons.second line 17
lemma OAI.SmoothObstruction.ShiftComparisons.first_injective line 19
lemma OAI.SmoothObstruction.ShiftComparisons.second_injective line 25
lemma OAI.SmoothObstruction.ShiftComparisons.no_loops line 28
def OAI.SmoothObstruction.ShiftComparisons.used line 45
Source documentation
Only the at-most-three sampled words actually present are charged by the probability bound, even when some input indices coincide.
```
def used {M : ℕ} (a b c : Fin M) : Finset (Fin M) := {a,b,c}
```
lemma OAI.SmoothObstruction.ShiftComparisons.used_nonempty line 47
lemma OAI.SmoothObstruction.ShiftComparisons.used_card line 49
def OAI.SmoothObstruction.ShiftComparisons.firstUsed line 55
def OAI.SmoothObstruction.ShiftComparisons.secondUsed line 60
lemma OAI.SmoothObstruction.ShiftComparisons.firstUsed_injective line 64
lemma OAI.SmoothObstruction.ShiftComparisons.secondUsed_injective line 68
lemma OAI.SmoothObstruction.ShiftComparisons.no_loops_used line 72
def OAI.SmoothObstruction.ShiftComparisons.matchCount line 83

theorem OAI.SmoothObstruction.ShiftComparisons.bad_probability line 88

Source documentation

Source shifted-comparison probability, including coincidences among all three selected sample-list indices.

theorem bad_probability {M N : ℕ} [NeZero N] (P : Law (Fin N → A))
    (a b c : Fin M) (t : Fin N) (h : t ≠ 0 ∨ a ≠ c) (d : ℕ) (hd : d ≤ N)
    {U : ℝ} (hU : 1 ≤ U) (hA : 1 ≤ (Fintype.card A : ℝ))
    (hP : ∀ w, P.mass w ≤ 2 * (U / Fintype.card A) ^ N) :
    prob (product (fun _ : Fin M => P)) (univ.filter (fun w => d ≤ matchCount w a b c t)) ≤
      8 * 2 ^ N * U ^ (3 * N) * (Fintype.card A : ℝ) ^ (-(d : ℝ) / 2) := by
…

Mentions: OAI.SmoothObstruction.ShiftComparisons.matchCount

abbrev OAI.SmoothObstruction.ShiftComparisons.Config line 107
lemma OAI.SmoothObstruction.ShiftComparisons.card_config line 110

theorem OAI.SmoothObstruction.ShiftComparisons.all_bad_probability line 119

Source documentation

Simultaneous bound for every aligned or shifted comparison in the actual M-word sample. The finite index set has at most N M³ members.

theorem all_bad_probability {M N : ℕ} [NeZero N] (P : Law (Fin N → A))
    (d : ℕ) (hd : d ≤ N) {U : ℝ} (hU : 1 ≤ U) (hA : 1 ≤ (Fintype.card A : ℝ))
    (hP : ∀ w, P.mass w ≤ 2 * (U / Fintype.card A) ^ N) :
    prob (product (fun _ : Fin M => P))
      (univ.biUnion (fun z : Config M N => univ.filter (fun w =>
        d ≤ matchCount w z.val.1 z.val.2.1 z.val.2.2.1 z.val.2.2.2))) ≤
      (N * M ^ 3 : ℝ) * (8 * 2 ^ N * U ^ (3 * N) *
        (Fintype.card A : ℝ) ^ (-(d : ℝ) / 2)) := by
…

Mentions: OAI.SmoothObstruction.ShiftComparisons.Config, OAI.SmoothObstruction.ShiftComparisons.matchCount

def OAI.SmoothObstruction.WordFamily.observableLaw line 144
def OAI.SmoothObstruction.WordFamily.empiricalTV line 147
lemma OAI.SmoothObstruction.WordFamily.empiricalTV_nonneg line 152
lemma OAI.SmoothObstruction.WordFamily.expectedTV line 157
lemma OAI.SmoothObstruction.WordFamily.window_bad_probability line 165
lemma OAI.SmoothObstruction.WordFamily.product_support line 180
lemma OAI.SmoothObstruction.WordFamily.injective_of_separation line 190

theorem OAI.SmoothObstruction.WordFamily.exists_family line 205

Source documentation

Actual simultaneous family selection. The two bad events are evaluated in one product law and support is preserved for each complete list.

theorem exists_family {M N d : ℕ} [NeZero M] [NeZero N]
    (P : Law (Fin N → A)) (f : I → (Fin N → A) → C)
    {U θ : ℝ} (hU : 1 ≤ U) (hA : 1 ≤ (Fintype.card A : ℝ)) (hθ : 0 < θ)
    (hd : d ≤ N) (hP : ∀ w, P.mass w ≤ 2 * (U / Fintype.card A) ^ N)
    (hwindow : Fintype.card I * ((1/2 : ℝ) * Real.sqrt (Fintype.card C / M)) / θ < 1/4)
    (hdistance : (N * M ^ 3 : ℝ) * (8 * 2 ^ N * U ^ (3 * N) *
      (Fintype.card A : ℝ) ^ (-(d : ℝ) / 2)) < 1/4) :
    ∃ w : Fin M → Fin N → A, Function.Injective w ∧
      (∀ i, 0 < P.mass (w i)) ∧
      (∀ i, empiricalTV P (f i) w ≤ θ) ∧
      ∀ a b c : Fin M, ∀ t : Fin N, t ≠ 0 ∨ a ≠ c → matchCount w a b c t < d := by
…

Mentions: OAI.SmoothObstruction.WordFamily.empiricalTV

def OAI.SmoothObstruction.FiniteLaw.transport line 245
lemma OAI.SmoothObstruction.FiniteLaw.expect_transport line 250
def OAI.SmoothObstruction.WordFlatten.flattenEquiv line 260
lemma OAI.SmoothObstruction.WordFlatten.full_test line 269
lemma OAI.SmoothObstruction.WordFlatten.expect_full_test line 285

lemma OAI.SmoothObstruction.WordFlatten.conditioned_mass line 297

Source documentation

Pointwise mass of the true constrained and once-conditioned complete list. This is derived from the arbitrary sublist estimate, not independence of constituent positions.

lemma conditioned_mass (hd : K+1 ≤ Module.finrank (ZMod 2) V) (hK : 1 ≤ K)
    (E : Finset (Fin q → Fin H → {v : V // v ≠ 0}))
    (hE : 1/2 ≤ prob (rawLaw B hd H q) E) (v : Fin q → Fin H → {v : V // v ≠ 0}) :
    (condition (rawLaw B hd H q) E (by change 0 < prob _ E; linarith)).mass v ≤
      2 * ((2 : ℝ) ^ (2*K) / Fintype.card {v : V // v ≠ 0}) ^ (q*H) := by
…

def OAI.SmoothObstruction.WordFlatten.flatLaw line 306
lemma OAI.SmoothObstruction.WordFlatten.flat_mass line 311
lemma OAI.SmoothObstruction.WordFlatten.flat_support line 318
lemma OAI.SmoothObstruction.WordFlatten.flat_relations line 325

theorem OAI.SmoothObstruction.WordFlatten.exists_family line 337

Source documentation

Complete supported family selection for the actual grouped symplectic sampler. Caller-specified observables encode the short windows, while E is the proved per-word approximation event.

theorem exists_family {M d : ℕ} [NeZero M] [NeZero (q*H)]
    {C I : Type*} [Fintype C] [DecidableEq C] [Fintype I]
    (hd : K+1 ≤ Module.finrank (ZMod 2) V) (hK : 1 ≤ K)
    (hA : 1 ≤ (Fintype.card {v : V // v ≠ 0} : ℝ))
    (E : Finset (Fin q → Fin H → {v : V // v ≠ 0}))
    (hE : 1/2 ≤ prob (rawLaw B hd H q) E)
    (f : I → (Fin (q*H) → {v : V // v ≠ 0}) → C)
    {θ : ℝ} (hθ : 0 < θ) (hmatch : d ≤ q*H)
    (hwindow : Fintype.card I * ((1/2 : ℝ) * Real.sqrt (Fintype.card C / M)) / θ < 1/4)
    (hdistance : ((q*H) * M^3 : ℝ) * (8 * 2^(q*H) * ((2 : ℝ)^(2*K))^(3*(q*H)) *
      (Fintype.card {v : V // v ≠ 0} : ℝ)^(-(d : ℝ)/2)) < 1/4) :
    ∃ w : Fin M → Fin (q*H) → {v : V // v ≠ 0}, Function.Injective w ∧
…

instance OAI.SmoothObstruction.WordStep.alphabetFintype line 370
instance OAI.SmoothObstruction.WordStep.alphabetDecidableEq line 371
def OAI.SmoothObstruction.WordStep.N line 373
def OAI.SmoothObstruction.WordStep.H line 374
def OAI.SmoothObstruction.WordStep.q line 375
def OAI.SmoothObstruction.WordStep.D line 376
lemma OAI.SmoothObstruction.WordStep.q_mul_H line 377
lemma OAI.SmoothObstruction.WordStep.N_pos line 379
lemma OAI.SmoothObstruction.WordStep.H_pos line 380
lemma OAI.SmoothObstruction.WordStep.q_pos line 381
instance OAI.SmoothObstruction.WordStep.qH_neZero line 382
lemma OAI.SmoothObstruction.WordStep.D_le_N line 383
lemma OAI.SmoothObstruction.WordStep.cardAlphabetReal line 385
lemma OAI.SmoothObstruction.WordStep.epsilon_le_one line 388
def OAI.SmoothObstruction.WordStep.matchThreshold line 392
lemma OAI.SmoothObstruction.WordStep.matchThreshold_le line 393
lemma OAI.SmoothObstruction.WordStep.le_matchThreshold line 396
abbrev OAI.SmoothObstruction.WordStep.Offsets line 399
Source documentation
Actual offset set for nonwrapping source D-windows.
```
abbrev Offsets (s : ℕ) := {t : Fin (q s * H s) // t.val+D s ≤ q s*H s}
```
Mentions: OAI.SmoothObstruction.WordStep.q, OAI.SmoothObstruction.WordStep.H, OAI.SmoothObstruction.WordStep.D
def OAI.SmoothObstruction.WordStep.window line 400
lemma OAI.SmoothObstruction.WordStep.card_offsets line 402
lemma OAI.SmoothObstruction.WordStep.window_budget line 405
lemma OAI.SmoothObstruction.WordStep.distance_budget line 422
lemma OAI.SmoothObstruction.WordStep.alphabetSize_ge_one line 460

theorem OAI.SmoothObstruction.WordStep.exists_step line 470

Source documentation

One actual finite-family selection at the exact source parameters. No distance, injectivity, window law or symplectic relation is an assumption; they are all supplied by the independent sample argument and checked budgets. The single per-word conditioning event is passed with its proved mass bound.

theorem exists_step {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s)
    (E : Finset (Fin (q s) → Fin (H s) → Alphabet s))
    (hE : 1/2 ≤ prob (rawLaw (form s) (by rw [finrank]; exact dimension_budget hk) (H s) (q s)) E) :
    ∃ w : Fin (Fintype.card (Alphabet (nextS i s))) → Fin (q s*H s) → Alphabet s,
      Function.Injective w ∧
      (∀ a, WordFlatten.flattenEquiv.symm (w a) ∈ E) ∧
      (∀ a b (r k : ℕ) (_hk : k<K s) (_hk8 : k ≤ K s/8) (hr : r+2^k<H s),
        form s (w a (finProdFinEquiv (b,⟨r,lt_trans (Nat.lt_add_of_pos_right (by positivity)) hr⟩))).val
          (w a (finProdFinEquiv (b,⟨r+2^k,hr⟩))).val = 0) ∧
      (∀ t, WordFamily.empiricalTV
        (WordFlatten.flatLaw (form s) (by rw [finrank]; exact dimension_budget hk) E hE)
        (window s t) w ≤ 1/10000) ∧
…

Mentions: OAI.SmoothObstruction.WordStep.q, OAI.SmoothObstruction.WordStep.H, OAI.SmoothObstruction.WordFamily.empiricalTV, OAI.SmoothObstruction.WordFlatten.flatLaw, OAI.SmoothObstruction.WordStep.window

theorem OAI.SmoothObstruction.WordStep.approximation_mass line 500

Source documentation

At successive exact source levels the per-word approximation event has probability at least a half, for every actual previous-window map.

theorem approximation_mass {i s : ℕ} (hk : 256 ≤ K s) (hε : 32 ≤ epsilon i * K s)
    (f : Offsets s → Alphabet (nextS i s) → (Fin (D s) → Alphabet s)) :
    1/2 ≤ prob (rawLaw (form (nextS i s))
      (by rw [finrank]; exact dimension_budget (by have := one_step_growth hk hε; omega))
…

Mentions: OAI.SmoothObstruction.WordStep.Offsets, OAI.SmoothObstruction.WordStep.D