SparseMoment.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.CoordinateSweeps.Grid.Holes.holeHeavy line 26
def OAI.CoordinateSweeps.Grid.Holes.particleHeavy line 29
def OAI.CoordinateSweeps.Grid.Holes.holeHeavyHits line 33
def OAI.CoordinateSweeps.Grid.Holes.particleHeavyHits line 36
theorem OAI.CoordinateSweeps.Grid.Holes.probability_holeHeavy_single line 39
theorem OAI.CoordinateSweeps.Grid.Holes.probability_holeHeavyHits_le line 59
theorem OAI.CoordinateSweeps.Grid.Holes.probability_particleHeavyHits_le line 70
theorem OAI.CoordinateSweeps.Grid.Holes.not_vertexIsolated_iff line 96
theorem OAI.CoordinateSweeps.Grid.Holes.not_good_cover line 120
theorem OAI.CoordinateSweeps.Grid.Holes.card_covered_by_good_and_bad line 144
theorem OAI.CoordinateSweeps.Grid.Holes.fewGood_cover line 171

theorem OAI.CoordinateSweeps.Grid.Holes.probability_fewGood_le line 202

Source comment

Source04:eq12 prior to choosing absolute parameters and absorbing subpolynomial factors. There is no conditioning on a particle-selected line set.

theorem probability_fewGood_le (H : G.Holes h) (hH : H.Feasible) {η : ℝ} (hη : 0 < η)
    (hh : 2*h/((G.size : ℝ)*η) ≤ 1) (hk : 2*k/((G.size : ℝ)*η) ≤ 1)
    (hv : ((k+h : ℕ) : ℝ)*G.vertexSharingRate ≤ 1) :
    Coverage.probability G.endpointWeight (fun p : Fin k → G.Slot × G.Slot =>
      ((H.goodSet (fun i => (p i).1) (fun i => (p i).2) η).card : ℝ) < k/2) ≤
      (2 : ℝ)^k * (((k+h : ℕ) : ℝ)*G.vertexSharingRate)^((k : ℝ)/8) +
      ∑ j : Fin G.b, ((2 : ℝ)^k * (2*h/((G.size : ℝ)*η))^((k : ℝ)/(8*G.b)) +
        ((Fintype.card (G.Line j)+1 : ℕ) : ℝ)^⌊2*k/(((2^G.bits j : ℕ) : ℝ)*η)⌋₊ *
          (2 : ℝ)^k * (2*k/((G.size : ℝ)*η))^((k : ℝ)/(8*G.b))) := by
…

Mentions: OAI.CoordinateSweeps.Coverage.probability

def OAI.CoordinateSweeps.Grid.Holes.uniformSparsePrefactor line 246
Source comment
An explicit absolute prefactor used before asymptotic absorption.
```
def uniformSparsePrefactor (G : Grid) (h k : ℕ) : ℝ :=
…
```
Mentions: OAI.CoordinateSweeps.Grid
theorem OAI.CoordinateSweeps.Grid.Holes.placementHSsq_uniform_le_fewGood line 251
Source comment
The source's good/bad entry split, in counting HS normalization.
```
theorem placementHSsq_uniform_le_fewGood (H : G.Holes h) {η : ℝ}
    (hη : 0 ≤ η) (hηsmall : η ≤ 1/8) :
    H.placementHSsq (k := k) (fun _ => FiniteLaw.uniform _) ≤
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform
abbrev OAI.CoordinateSweeps.Grid.Holes.InputPlacements line 327
abbrev OAI.CoordinateSweeps.Grid.Holes.OutputPlacements line 328
def OAI.CoordinateSweeps.Grid.Holes.placementTop line 330
def OAI.CoordinateSweeps.Grid.Holes.transitionMatrix line 333
theorem OAI.CoordinateSweeps.Grid.Holes.extraProbability_dependsOn line 338
theorem OAI.CoordinateSweeps.Grid.Holes.alternatingKernel_eq_placementKernel line 352
theorem OAI.CoordinateSweeps.Grid.Holes.placementHSsq_eq_subtype line 360

theorem OAI.CoordinateSweeps.Grid.Holes.transitionMatrix_top_norm_le line 385

Source comment

Exact top-placement restriction of the ACTUAL conditioned sweep, bounded by the already proved path-weight Q counting norm. No representation-theoretic conclusion is inserted as a hypothesis.

theorem transitionMatrix_top_norm_le (H : G.Holes h)
    (μ : ∀ j, FiniteLaw (Equiv.Perm (Cube (G.bits j))))
    (v : EuclideanSpace ℂ (H.OutputPlacements k))
    (hv : (fun y => v y) ∈ H.placementTop k) :
    ‖(EuclideanSpace.equiv (H.InputPlacements k) ℂ).symm ((H.transitionMatrix μ).mulVec v)‖ ≤
      Real.sqrt (H.placementHSsq (k := k) μ) * ‖v‖ := by
…

Mentions: OAI.CoordinateSweeps.FiniteLaw, OAI.CoordinateSweeps.Cube