SecondMomentAssembly.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.weightedCorrelation line 9
Source documentation
Finite weighted pair correlation, with no probability-library dependency.
```
def weightedCorrelation {Ω I : Type*} [Fintype Ω]
    (w : Ω → ℝ) (z : Ω → I → ℂ) (i j : I) : ℂ :=
…
```
theorem OAI.Problem337.norm_sum_sq_eq_sum_pair line 13
theorem OAI.Problem337.weighted_second_moment_identity line 22

theorem OAI.Problem337.second_moment_exceptional_bound line 33

Source documentation

Exceptional pairs cost their cardinality; all other pairs cost the common correlation bound. The assumptions deliberately expose the exact analytic interface.

theorem second_moment_exceptional_bound {Ω I : Type*} [Fintype Ω] [Fintype I]
    (w : Ω → ℝ) (z : Ω → I → ℂ) (E : Finset (I × I)) (δ : ℝ) (hδ : 0 ≤ δ)
    (hall : ∀ i j, ‖weightedCorrelation w z i j‖ ≤ 1)
    (hgood : ∀ i j, (i, j) ∉ E → ‖weightedCorrelation w z i j‖ ≤ δ) :
    (∑ ω, w ω * ‖∑ i, z ω i‖ ^ 2) ≤
      (E.card : ℝ) + (Fintype.card I : ℝ) ^ 2 * δ := by
…

Mentions: OAI.Problem337.weightedCorrelation

theorem OAI.Problem337.weightedCorrelation_norm_le_one line 56

Source documentation

Correlations of unit-bounded variables under nonnegative weights of mass one are themselves bounded by one.

theorem weightedCorrelation_norm_le_one {Ω I : Type*} [Fintype Ω]
    (w : Ω → ℝ) (z : Ω → I → ℂ) (hw : ∀ ω, 0 ≤ w ω)
    (hmass : ∑ ω, w ω = 1) (hz : ∀ ω i, ‖z ω i‖ ≤ 1) (i j : I) :
    ‖weightedCorrelation w z i j‖ ≤ 1 := by
…

Mentions: OAI.Problem337.weightedCorrelation

theorem OAI.Problem337.boolean_second_moment_bound line 75

Source documentation

The random-products second-moment reduction: after the separated-pair correlation estimate, the only loss is the exponentially small Hamming exception.

theorem boolean_second_moment_bound {Ω : Type*} [Fintype Ω] (m : ℕ)
    (w : Ω → ℝ) (z : Ω → (Fin m → Bool) → ℂ)
    (hw : ∀ ω, 0 ≤ w ω) (hmass : ∑ ω, w ω = 1)
    (hz : ∀ ω i, ‖z ω i‖ ≤ 1) (δ : ℝ) (hδ : 0 ≤ δ)
    (hgood : ∀ i j, (m : ℝ) / 4 ≤ (hammingDist i j : ℝ) →
      ‖weightedCorrelation w z i j‖ ≤ δ) :
    (∑ ω, w ω * ‖∑ i, z ω i‖ ^ 2) / (4 : ℝ) ^ m ≤
      Real.exp (-(m : ℝ) / 16) + δ := by
…

Mentions: OAI.Problem337.weightedCorrelation

theorem OAI.Problem337.weighted_exposure_bound line 103

Source documentation

Averaging over exposed variables costs at most the mass of bad exposures plus the bound that holds uniformly on the good exposures.

theorem weighted_exposure_bound {Ω : Type*} [Fintype Ω]
    (w : Ω → ℝ) (f : Ω → ℂ) (B : Finset Ω) (a b : ℝ)
    (hw : ∀ ω, 0 ≤ w ω) (hmass : ∑ ω, w ω = 1)
    (ha : 0 ≤ a) (hbad : ∑ ω ∈ B, w ω ≤ b)
    (hall : ∀ ω, ‖f ω‖ ≤ 1) (hgood : ∀ ω, ω ∉ B → ‖f ω‖ ≤ a) :
    ‖∑ ω, (w ω : ℂ) * f ω‖ ≤ a + b := by
…

theorem OAI.Problem337.random_second_moment_absorption line 127

Source documentation

The numerical absorption at the end of the random-products argument.

theorem random_second_moment_absorption (m V : ℝ) (hlarge : 50 ≤ min m V) :
    Real.exp (-m / 16) + Real.exp (-V / 20) + Real.exp (-V / 5) ≤
      Real.exp (-min m V / 100) := by
…

theorem OAI.Problem337.boolean_random_second_moment_bound line 157

Source documentation

Final second-moment estimate once the good/bad pair-exposure estimates are supplied. All constants agree with the random-products lemma.

theorem boolean_random_second_moment_bound {Ω : Type*} [Fintype Ω] (m : ℕ) (V : ℝ)
    (w : Ω → ℝ) (z : Ω → (Fin m → Bool) → ℂ)
    (hw : ∀ ω, 0 ≤ w ω) (hmass : ∑ ω, w ω = 1)
    (hz : ∀ ω i, ‖z ω i‖ ≤ 1) (hlarge : 50 ≤ min (m : ℝ) V)
    (hgood : ∀ i j, (m : ℝ) / 4 ≤ (hammingDist i j : ℝ) →
      ‖weightedCorrelation w z i j‖ ≤ Real.exp (-V / 20) + Real.exp (-V / 5)) :
    (∑ ω, w ω * ‖∑ i, z ω i‖ ^ 2) / (4 : ℝ) ^ m ≤
      Real.exp (-min (m : ℝ) V / 100) := by
…

Mentions: OAI.Problem337.weightedCorrelation