OAI/Probability/CoordinateSweeps/SparseBound.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.SparseScalar.theta line 34

   Source comment

   A concrete permissible choice in source04/06. R is still chosen last.

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:260 (same declaration text).

   def theta : ℝ := 1/1600

2. def OAI.CoordinateSweeps.SparseScalar.K0 line 35

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:261 (same declaration text).

3. def OAI.CoordinateSweeps.SparseScalar.B0 line 36

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:262 (same declaration text).

4. def OAI.CoordinateSweeps.SparseScalar.xi line 37

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:263 (same declaration text).

5. def OAI.CoordinateSweeps.SparseScalar.rho line 38

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:264 (same declaration text).

6. def OAI.CoordinateSweeps.SparseScalar.q line 39

   Also declared: ComparatorChallenges/CoordinateSweeps.lean:265 (same declaration text).

7. lemma OAI.CoordinateSweeps.SparseScalar.constants line 40
8. lemma OAI.CoordinateSweeps.SparseScalar.pow_two_exp line 43
9. lemma OAI.CoordinateSweeps.SparseScalar.exp_rpow line 45
10. lemma OAI.CoordinateSweeps.SparseScalar.rpow_exp line 47
11. lemma OAI.CoordinateSweeps.SparseScalar.eventually_power_gt line 49
12. lemma OAI.CoordinateSweeps.SparseScalar.eventually_log_le_power line 51
13. lemma OAI.CoordinateSweeps.SparseScalar.eventually_sparse_requirements line 60

    Source comment

    All scalar scale requirements for the sparse proof can be imposed before R and the finite real perturbation interval are fixed.

    lemma eventually_sparse_requirements :
        ∀ᶠ s : ℝ in atTop, 1 < s ∧
          Real.log s ≤ s^(theta/4) ∧ 2 ≤ s^(theta/4) ∧
          (B0+1 : ℝ) ≤ s^(theta/2) ∧
          4/s^(1/(4*(B0:ℝ))) ≤ theta/(64*B0) ∧
          Real.log (2*(B0:ℝ)+1)+Real.log 2 ≤ xi*Real.log s ∧
          Real.log 2 ≤ xi*Real.log s/8 := by
    …

    Mentions: OAI.CoordinateSweeps.SparseScalar.theta, OAI.CoordinateSweeps.SparseScalar.B0, OAI.CoordinateSweeps.SparseScalar.xi

14. lemma OAI.CoordinateSweeps.SparseScalar.many_HS_bound line 86

    Source comment

    Arithmetic behind the many-coordinate HS bound, with its full literal prefactor. The inputs are scalar size bounds derived from the allowed grid.

    lemma many_HS_bound (s t b h : ℝ) (k : ℕ) (hs : 1 < s) (ht : 0 ≤ t)
        (hts : t ≤ s^(-theta/2)) (hh : h ≤ K0*k)
        (hb : 0 ≤ b)
        (habsorb : 3*Real.log 2+2*b*(K0+1+Real.log 4) ≤ theta*Real.log s/8) :
        ((2:ℝ)^k*Real.exp (b*(h+k)+Real.log 4*k*b))^2 *
          ((2:ℝ)^k*t^((k:ℝ)/2)) ≤ s^(-theta*k/8) := by
    …

    Mentions: OAI.CoordinateSweeps.SparseScalar.theta, OAI.CoordinateSweeps.SparseScalar.K0

15. lemma OAI.CoordinateSweeps.SparseScalar.prob_power_bound line 110
16. lemma OAI.CoordinateSweeps.SparseScalar.fewGood_bound line 126

    Source comment

    Scalar absorption of the literal coverage/occupancy union estimate.

    lemma fewGood_bound {b k : ℕ} (hb : 1 ≤ b) (hB : b ≤ B0) (hk : 1 ≤ k)
        {s v u t : ℝ} (hs : 1 < s) (hv : 0 ≤ v) (hu : 0 ≤ u) (ht : 0 ≤ t)
        (hvs : v ≤ s^(-theta/2)) (hus : u ≤ s^(-theta/2)) (hts : t ≤ s^(-theta/2))
        (C : Fin b → ℝ) (hC0 : ∀ j, 0 ≤ C j)
        (hC : ∀ j, C j ≤ Real.exp (theta*k*Real.log s/(32*B0)))
        (habs : Real.log (1+2*(B0:ℝ))+Real.log 2 ≤ xi*Real.log s) :
        (2:ℝ)^k*v^((k:ℝ)/8)+∑ j : Fin b,
          ((2:ℝ)^k*u^((k:ℝ)/(8*b))+C j*2^k*t^((k:ℝ)/(8*b))) ≤ s^(-xi*k) := by
    …

    Mentions: OAI.CoordinateSweeps.SparseScalar.B0, OAI.CoordinateSweeps.SparseScalar.theta, OAI.CoordinateSweeps.SparseScalar.xi

17. lemma OAI.CoordinateSweeps.Grid.size_pos line 185
18. lemma OAI.CoordinateSweeps.Grid.log_size line 186
19. lemma OAI.CoordinateSweeps.Grid.log_size_lower line 190
20. lemma OAI.CoordinateSweeps.Grid.log_size_upper line 197
21. lemma OAI.CoordinateSweeps.Grid.log_coordinate line 209
22. lemma OAI.CoordinateSweeps.Grid.log_size_pos_of_allowed line 211
23. lemma OAI.CoordinateSweeps.Grid.coordinate_log_many line 216
24. lemma OAI.CoordinateSweeps.Grid.coordinate_log_bounded line 230
25. lemma OAI.CoordinateSweeps.Grid.coordinate_size_many line 243
26. lemma OAI.CoordinateSweeps.Grid.coordinate_size_bounded line 249
27. lemma OAI.CoordinateSweeps.Grid.card_line_mul line 256
28. lemma OAI.CoordinateSweeps.Grid.card_line_le line 260
29. lemma OAI.CoordinateSweeps.SparseScalar.sparse_fraction line 266
30. lemma OAI.CoordinateSweeps.SparseScalar.sparse_line_mass line 281
31. lemma OAI.CoordinateSweeps.SparseScalar.logarithm_count line 293
32. lemma OAI.CoordinateSweeps.SparseScalar.occupancy_count line 302
33. lemma OAI.CoordinateSweeps.SparseScalar.sparse_vertex_fraction line 332
34. theorem OAI.CoordinateSweeps.Grid.Holes.sparse_fewGood_bound line 350

    Source comment

    Uniform bounded-axis source04:eq12, with all sparse geometry now discharged.

    theorem sparse_fewGood_bound (hf : H.Feasible) {r : ℕ} (hG : G.Allowed r)
        (hb : G.b ≤ B0) (hk : 1 ≤ k) (hs : (2:ℝ) ≤ G.size)
        (hsp : ((h+k:ℕ):ℝ) ≤ (G.size:ℝ)^(1-theta))
        (h2 : 2 ≤ (G.size:ℝ)^(theta/4)) (hB : (B0+1:ℝ) ≤ (G.size:ℝ)^(theta/2))
        (hcount : 4/(G.size:ℝ)^(1/(4*(B0:ℝ))) ≤ theta/(64*B0))
        (habs : Real.log (1+2*(B0:ℝ))+Real.log 2 ≤ xi*Real.log G.size) :
        Coverage.probability G.endpointWeight (fun v : Fin k → G.Slot × G.Slot =>
          ((H.goodSet (fun i => (v i).1) (fun i => (v i).2) ((G.size:ℝ)^(-xi))).card:ℝ)<k/2) ≤
          (G.size:ℝ)^(-xi*k) := by
    …

    Mentions: OAI.CoordinateSweeps.Coverage.probability

35. def OAI.CoordinateSweeps.SparseScalar.uniformRate line 384

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:267 (same declaration text).

36. lemma OAI.CoordinateSweeps.SparseScalar.uniformRate_nonneg line 388
37. lemma OAI.CoordinateSweeps.SparseScalar.eventually_prefactor_small line 397
38. lemma OAI.CoordinateSweeps.Grid.Holes.uniformSparsePrefactor_le line 407
39. theorem OAI.CoordinateSweeps.Grid.Holes.sparse_uniform_HS_bound line 432

    Source comment

    Quantitative uniform-law HS-square contraction with fixed slack for the later finite real perturbation step.

    theorem sparse_uniform_HS_bound (H : G.Holes h) (hf : H.Feasible) {r : ℕ} (hG : G.Allowed r)
        (hb : G.b ≤ B0) (hk : 1 ≤ k) (hh : (h:ℝ) ≤ K0*k) (hs : (2:ℝ) ≤ G.size)
        (hsp : ((h+k:ℕ):ℝ) ≤ (G.size:ℝ)^(1-theta))
        (h2 : 2 ≤ (G.size:ℝ)^(theta/4)) (hB : (B0+1:ℝ) ≤ (G.size:ℝ)^(theta/2))
        (hcount : 4/(G.size:ℝ)^(1/(4*(B0:ℝ))) ≤ theta/(64*B0))
        (habs : Real.log (1+2*(B0:ℝ))+Real.log 2 ≤ xi*Real.log G.size)
        (hη : (G.size:ℝ)^(-xi) ≤ 1/8)
        (hpref : uniformRate ≤ xi*Real.log G.size/16) (hlog2 : Real.log 2 ≤ xi*Real.log G.size/8) :
        H.placementHSsq (k := k) (fun _ => FiniteLaw.uniform _) ≤ (G.size:ℝ)^(-xi*k/4) := by
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform

40. lemma OAI.CoordinateSweeps.Grid.b_le_log_size line 488
41. lemma OAI.CoordinateSweeps.Grid.sparse_lineSharing line 491
42. lemma OAI.CoordinateSweeps.Grid.sparse_many_absorb line 518
43. theorem OAI.CoordinateSweeps.Grid.Holes.sparse_many_HS_bound line 533

    Source comment

    Literal many-coordinate real-law HS-square bound, with all grid and forest-counting conditions derived from source sparse size assumptions.

    theorem sparse_many_HS_bound (H : G.Holes h) (hf : H.Feasible) {r : ℕ}
        (hr : 1 ≤ r) (hG : G.Allowed r) (hb : B0 ≤ G.b)
        (hrL : 1 ≤ (r:ℝ)*Real.log 2)
        (hrA : 3*Real.log 2+2*(K0+1+Real.log 4) ≤ theta*((r:ℝ)*Real.log 2)/8)
        (hh : (h:ℝ) ≤ K0*k)
        (hlog : Real.log G.size ≤ (G.size:ℝ)^(theta/4))
        (hsp : ((h+k:ℕ):ℝ) ≤ (G.size:ℝ)^(1-theta))
        {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
        (hlo : ∀ j g, (1/2:ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
        (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g) :
        H.placementHSsq (k := k) (fun j => lineLaw (G.bits j) z hz hz') ≤
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw

44. lemma OAI.CoordinateSweeps.Grid.continuous_choiceWeight line 557

    Source comment

    Every choice mass is a real polynomial. No conditional law is extended to complex z.

    lemma continuous_choiceWeight (G : Grid) (ω : G.Choices) : Continuous (fun z : ℝ => G.choiceWeight z ω) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid

45. def OAI.CoordinateSweeps.Grid.eventDistance line 562

    Source comment

    Event-level l1 distance, independent of the representation and therefore suitable for a single bounded-grid perturbation interval.

    Also declared: ComparatorChallenges/CoordinateSweeps.lean:191 (same declaration text).

    def eventDistance (G : Grid) (E : Finset G.Choices) (z : ℝ) : ℝ :=
    …

    Mentions: OAI.CoordinateSweeps.Grid

46. lemma OAI.CoordinateSweeps.Grid.eventMass_zero_pos line 565
47. lemma OAI.CoordinateSweeps.Grid.continuousAt_eventDistance_zero line 568
48. lemma OAI.CoordinateSweeps.Grid.eventDistance_zero line 578
49. lemma OAI.CoordinateSweeps.Grid.eventually_eventDistance_small line 580
50. def OAI.CoordinateSweeps.Grid.Holes.event line 593
51. lemma OAI.CoordinateSweeps.Grid.Holes.event_nonempty line 594
52. lemma OAI.CoordinateSweeps.Grid.Holes.probability_eq_eventMass line 597
53. lemma OAI.CoordinateSweeps.Grid.Holes.eventDistance_eq line 600
54. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_difference_le line 609

    Source comment

    Uniform in every irreducible: real event-distance controls the conditional operator difference. This avoids choosing a topology on equivalence classes of irreducible models.

    theorem conditionalAverage_difference_le (H : G.Holes h) (hf : H.Feasible)
        (z : ℝ) (ρ : UnitaryIrrep H.stabilizer) :
        ‖H.conditionalAverage hf z ρ-H.conditionalAverage hf 0 ρ‖ ≤ G.eventDistance H.event z := by
    …

    Mentions: OAI.CoordinateSweeps.UnitaryIrrep

55. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_perturb_bound line 619
56. def OAI.CoordinateSweeps.Grid.BoundedCode line 631

    Source comment

    Literal finite parameter space of bounded ordered grids; no model of irreducibles or of conditioned complex measures is involved.

    def BoundedCode (B r : ℕ) := Σ b : Fin (B+1),
    …

57. instance OAI.CoordinateSweeps.Grid.(instance at line 633) line 633
58. def OAI.CoordinateSweeps.Grid.BoundedCode.grid line 634
59. def OAI.CoordinateSweeps.Grid.boundedCode line 638
60. lemma OAI.CoordinateSweeps.Grid.boundedCode_grid line 640
61. theorem OAI.CoordinateSweeps.Grid.bounded_event_interval line 644

    Source comment

    Uniform finite real perturbation for all nonempty events on every bounded allowed grid. Quantifiers include all feasible path events, uniformly in h.

    theorem bounded_event_interval (B r : ℕ) (ε : Grid → ℝ) (hε : ∀ G, 0 < ε G) :
        ∃ zStar : ℝ, 0 < zStar ∧ zStar ≤ 1/2 ∧
          ∀ G : Grid, G.b ≤ B → (∀ j, G.bits j ≤ 2*r) →
          ∀ z ∈ Set.Icc 0 zStar, ∀ E : Finset G.Choices, E.Nonempty → G.eventDistance E z < ε G := by
    …

    Mentions: OAI.CoordinateSweeps.Grid