OAI/Analysis/FactorGeneration/PatchingBounds.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Generator.Tracial.patchingTolerance line 12
2. theorem OAI.Generator.Tracial.patchingTolerance_zero line 16
3. theorem OAI.Generator.Tracial.patchingTolerance_succ line 17
4. theorem OAI.Generator.Tracial.patchingTolerance_pos line 20
5. theorem OAI.Generator.Tracial.patchingTolerance_four_mul_le line 26
6. theorem OAI.Generator.Tracial.patchingTolerance_mono line 35
7. theorem OAI.Generator.Tracial.middleMomentError_nonneg line 42
8. theorem OAI.Generator.Tracial.patchingTolerance_middle_budget line 50

   Source documentation

   Choose eta=delta/3. Both middle moments fit within 2 epsilon_(r+2)/3.

   theorem patchingTolerance_middle_budget (δ : ℝ) (hδ : 0 < δ) (r : ℕ) :
       δ/3+(middleMomentError (patchingTolerance δ) r+patchingTolerance δ (r+2))/3 ≤
         2*patchingTolerance δ (r+2)/3 := by
   …

   Mentions: OAI.Generator.Tracial.middleMomentError, OAI.Generator.Tracial.patchingTolerance

9. def OAI.Generator.Tracial.binaryMasks line 73
10. theorem OAI.Generator.Tracial.mem_binaryMasks line 77
11. theorem OAI.Generator.Tracial.binaryMasks_length line 86
12. def OAI.Generator.Tracial.maskedWord line 91
13. theorem OAI.Generator.Tracial.patchingExpansion_eq_masks line 97
14. theorem OAI.Generator.Tracial.maskedWord_append line 106
15. theorem OAI.Generator.Tracial.maskedWord_no_patch line 117
16. theorem OAI.Generator.Tracial.maskedWord_norm_le_one line 124
17. theorem OAI.Generator.Tracial.exists_first_true line 141

    Source documentation

    Locate the first patch, with no earlier patch occurrences.

    theorem exists_first_true (bs : List Bool) (h : 1 ≤ bs.count true) :
        ∃ i cs,bs=List.replicate i false++true::cs := by
    …

18. theorem OAI.Generator.Tracial.exists_first_two_true line 153

    Source documentation

    Locate the first two patches; all bits before and between them are false.

    theorem exists_first_two_true (bs : List Bool) (h : 2 ≤ bs.count true) :
        ∃ i r cs,bs=List.replicate i false++true::(List.replicate r false++true::cs) := by
    …

19. theorem OAI.Generator.Tracial.first_two_full_length_iff line 163

    Source documentation

    The second moment has full word length only for the two-endpoint mask.

    theorem first_two_full_length_iff (i r : ℕ) (cs : List Bool) :
        r+2=(List.replicate i false++true::(List.replicate r false++true::cs)).length ↔
          i=0 ∧ cs=[] := by
    …

20. theorem OAI.Generator.Tracial.first_two_other_length line 170
21. theorem OAI.Generator.Tracial.binaryMasks_nodup line 184
22. theorem OAI.Generator.Tracial.count_true_zero_iff line 196
23. def OAI.Generator.Tracial.exceptionalMask line 202
24. theorem OAI.Generator.Tracial.exceptionalMask_eq line 204
25. theorem OAI.Generator.Tracial.first_two_eq_exceptional line 208
26. theorem OAI.Generator.Tracial.sum_indicator_le line 217
27. theorem OAI.Generator.Tracial.sum_three_budgets line 233
28. theorem OAI.Generator.Tracial.patchingTolerance_mask_budget line 262

    Source documentation

    The coarse ordinary+exceptional budget is exactly epsilon_k. The two special masks are each counted only once; no binomial count is assumed.

    theorem patchingTolerance_mask_budget (δ : ℝ) (k : ℕ) (hk : 1 ≤ k) :
        (2^k : ℝ)*(2*patchingTolerance δ (k-1)/3)+2*patchingTolerance δ k/3 =
          patchingTolerance δ k := by
    …

    Mentions: OAI.Generator.Tracial.patchingTolerance

29. theorem OAI.Generator.Tracial.exists_list_split line 279
30. theorem OAI.Generator.Tracial.exists_list_split_two line 293
31. theorem OAI.Generator.Tracial.patchingCoefficients_before line 301
32. theorem OAI.Generator.Tracial.patchingCoefficients_middle line 317
33. theorem OAI.Generator.Tracial.maskedWord_first_two line 325
34. theorem OAI.Generator.Tracial.maskedWord_two_decomposition line 339

    Source documentation

    Every mask with at least two true bits yields its actual internal middle segment, with no assumptions about a separately supplied finite list.

    theorem maskedWord_two_decomposition (F : Set M.toStarSubalgebra)
        (xs : List (Bool × M.toStarSubalgebra)) (hc : patchingCoefficients F xs)
        (bs : List Bool) (hlen : bs.length=xs.length) (hcount : 2 ≤ bs.count true) :
        ∃ pre a mid b post cs,
          xs=pre++a::(mid++b::post) ∧
          bs=List.replicate pre.length false++true::(List.replicate mid.length false++true::cs) ∧
          a.2 ∈ F ∧ (∀ c ∈ mid,c.2 ∈ F) ∧ cs.length=post.length ∧
          mid.length+2 ≤ xs.length := by
    …

    Mentions: OAI.Generator.Tracial.patchingCoefficients

35. theorem OAI.Generator.Tracial.maskedWord_one line 359
36. theorem OAI.Generator.Tracial.trace_list_sum line 374
37. theorem OAI.Generator.Tracial.norm_list_sum_le line 380
38. theorem OAI.Generator.Tracial.patching_trace_sum_le line 386