SparseLaw.lean`

37 declarations, 0 contain sorry, 0 declared as axioms

The finite calculation behind v2 Lemma projected-tv. The three singleton lines are averaged before the divergence is taken; projection choices are not part of the compared sample space. Coordinates are independently sampled occurrences, irrespective of whether their equation IDs coincide.

def OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights line 22
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights_pos line 25
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights_isProbability line 28
def OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare line 37
Source documentation
Pearson divergence against the uniform law, written with its constant denominator cleared. uniformChiSquare_eq_pearson identifies the actual likelihood-ratio definition.
```
def uniformChiSquare (p : α → ℝ) : ℝ :=
…
```
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare_eq_pearson line 40
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare_eq_secondMoment line 50
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare_nonneg line 66
def OAI.MaxCutGames.Decoder.SparseLaw.mixture line 70
theorem OAI.MaxCutGames.Decoder.SparseLaw.mixture_isProbability line 73
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare_mixture line 83
theorem OAI.MaxCutGames.Decoder.SparseLaw.totalVariation_le_half_sqrt line 93
def OAI.MaxCutGames.Decoder.SparseLaw.independentWeights line 102
theorem OAI.MaxCutGames.Decoder.SparseLaw.independentWeights_isProbability line 105
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare_independent line 113
theorem OAI.MaxCutGames.Decoder.SparseLaw.pow_mul_one_sub_le_one line 129
Source documentation
A finite bound sufficient for the cube asymptotic, without introducing a limit theorem or choosing the alphabet after the repetition count.
```
theorem pow_mul_one_sub_le_one (x : ℝ) (hx : 0 ≤ x) (k : ℕ) :
    (1 + x) ^ k * (1 - k * x) ≤ 1 := by
…
```
theorem OAI.MaxCutGames.Decoder.SparseLaw.pow_sub_one_le_fraction line 140
theorem OAI.MaxCutGames.Decoder.SparseLaw.pow_sub_one_le_twice line 147
def OAI.MaxCutGames.Decoder.SparseLaw.lineCount line 161
Source documentation
At the origin all three singleton lines contribute.
```
def lineCount (z : V × V) : ℝ :=
…
```
def OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights line 166
Source documentation
The average of the laws of (a,0), (0,a), and (a,a) for uniform a.
```
def singletonPairWeights (z : V × V) : ℝ := lineCount V z / (3 * Fintype.card V)
```
Mentions: OAI.MaxCutGames.Decoder.SparseLaw.lineCount
def OAI.MaxCutGames.Decoder.SparseLaw.singletonSamplerWeights line 170
Source documentation
Explicit finite pushforward of the three equally likely singleton choices. The same uniform slope supplies both entries of the diagonal choice.
```
def singletonSamplerWeights (z : V × V) : ℝ :=
…
```
theorem OAI.MaxCutGames.Decoder.SparseLaw.singletonSamplerWeights_eq line 175
theorem OAI.MaxCutGames.Decoder.SparseLaw.lineCount_sum line 202
theorem OAI.MaxCutGames.Decoder.SparseLaw.lineCount_sq line 216
theorem OAI.MaxCutGames.Decoder.SparseLaw.lineCount_sq_sum line 221
theorem OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights_isProbability line 232
theorem OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights_secondMoment line 241
theorem OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights_chiSquare line 247
theorem OAI.MaxCutGames.Decoder.SparseLaw.paddedSlope_chiSquare line 257
Source documentation
Exact finite divergence of the padded slope law.
```
theorem paddedSlope_chiSquare (β : ℝ) (hβ : 0 ≤ β) (hβ' : β ≤ 1) (k : ℕ) :
    uniformChiSquare (independentWeights (mixture β (singletonPairWeights V)) k) =
      (1 + β ^ 2 * ((Fintype.card V : ℝ) - 1) / 3) ^ k - 1 := by
…
```
Mentions: OAI.MaxCutGames.Decoder.SparseLaw.uniformChiSquare, OAI.MaxCutGames.Decoder.SparseLaw.independentWeights, OAI.MaxCutGames.Decoder.SparseLaw.mixture, OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights
theorem OAI.MaxCutGames.Decoder.SparseLaw.paddedSlope_totalVariation line 265
theorem OAI.MaxCutGames.Decoder.SparseLaw.paddedSlope_totalVariation_small line 272
theorem OAI.MaxCutGames.Decoder.SparseLaw.cubeSlope_totalVariation line 285
theorem OAI.MaxCutGames.Decoder.SparseLaw.exists_cubeSlope_totalVariation_le line 319
Source documentation
Arbitrarily many expected singleton coordinates coexist with arbitrarily small variation error: taking k=m³ and beta=m⁻² leaves k*beta=m. The bound involves only the fixed alphabet and requested error.
```
theorem exists_cubeSlope_totalVariation_le (η : ℝ) (hη : 0 < η) (N : ℕ) :
    ∃ m : ℕ, N ≤ m ∧ 0 < m ∧
      totalVariation
        (independentWeights (mixture (1 / (m : ℝ) ^ 2) (singletonPairWeights V)) (m ^ 3))
        (uniformWeights (Fin (m ^ 3) → V × V)) ≤ η := by
…
```
Mentions: OAI.MaxCutGames.Decoder.SparseLaw.independentWeights, OAI.MaxCutGames.Decoder.SparseLaw.mixture, OAI.MaxCutGames.Decoder.SparseLaw.singletonPairWeights, OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights
theorem OAI.MaxCutGames.Decoder.SparseLaw.cube_expected_singletons line 346
theorem OAI.MaxCutGames.Decoder.SparseLaw.translated_uniform_intercept line 360
Source documentation
Pulling back an independent uniform intercept through any translation, even one depending on all slopes and projection choices, leaves its joint law unchanged. No independence of that translation from the slopes is assumed.
```
theorem translated_uniform_intercept (p : α → ℝ) (shift : α → V) (a : α) (z : V) :
    p a * uniformWeights V (z - shift a) = p a * uniformWeights V z := rfl
```
Mentions: OAI.MaxCutGames.Decoder.SparseLaw.uniformWeights
theorem OAI.MaxCutGames.Decoder.SparseLaw.uniform_intercept_pushforward line 363
theorem OAI.MaxCutGames.Decoder.SparseLaw.joint_intercept_pushforward line 370
theorem OAI.MaxCutGames.Decoder.SparseLaw.totalVariation_append_uniform_intercept line 383