Degree.lean`

45 declarations, 0 contain sorry, 0 declared as axioms

Real Walsh analysis on finite Boolean cubes. The basis and inversion identities are proved from the explicit coordinate characters.

def OAI.OptimalMaxCut.Analytic.degree line 18
Source documentation
Frequency degree: cardinality of the set of selected Boolean coordinates.
```
def degree {I : Type*} [Fintype I] (s : Cube I) : ℕ :=
…
```
def OAI.OptimalMaxCut.Analytic.stability line 21
def OAI.OptimalMaxCut.Analytic.influence line 26
Source documentation
Full influence, with the same probability normalization.
```
noncomputable def influence {I : Type*} [Fintype I] [DecidableEq I]
    (i : I) (f : Cube I → ℝ) : ℝ :=
…
```
def OAI.OptimalMaxCut.Analytic.cutoffInfluence line 30
def OAI.OptimalMaxCut.Analytic.noise line 37
Source documentation
Ordinary Boolean noise in its exact Walsh multiplier representation. Range/mean preservation must be proved, not imposed as assumptions.
```
noncomputable def noise {I : Type*} [Fintype I] [DecidableEq I]
    (u : ℝ) (f : Cube I → ℝ) (x : Cube I) : ℝ :=
…
```
def OAI.OptimalMaxCut.Analytic.MajorityIsStablest line 41
def OAI.OptimalMaxCut.Analytic.UntruncatedMajorityIsStablest line 49
theorem OAI.OptimalMaxCut.Analytic.coefficient_noise line 62
Source documentation
Exact diagonalization of ordinary bit noise.
```
theorem coefficient_noise (u : ℝ) (f : Cube I → ℝ) (a : Cube I) :
    coefficient (noise u f) a = u ^ degree a * coefficient f a := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.noise, OAI.OptimalMaxCut.Analytic.degree
theorem OAI.OptimalMaxCut.Analytic.spectral_energy_le_one line 72
Source documentation
The finite energy bound used for the dimension-independent cutoff step.
```
theorem spectral_energy_le_one (f : Cube I → ℝ)
    (hf : ∀ x, -1 ≤ f x ∧ f x ≤ 1) :
    (∑ s, coefficient f s ^ 2) ≤ 1 := by
…
```
theorem OAI.OptimalMaxCut.Analytic.stability_noise line 81
theorem OAI.OptimalMaxCut.Analytic.stability_noise_le line 92
Source documentation
Noise only decreases nonnegative stability (lem:mis, first inequality).
```
theorem stability_noise_le (t u : ℝ) (ht : 0 ≤ t) (hu : 0 ≤ u) (hu1 : u ≤ 1)
    (f : Cube I → ℝ) : stability t (noise u f) ≤ stability t f := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.stability, OAI.OptimalMaxCut.Analytic.noise
theorem OAI.OptimalMaxCut.Analytic.stability_sub_noise line 103
Source documentation
The exact error integrand, before replacing it by any uniform bound.
```
theorem stability_sub_noise (t u : ℝ) (f : Cube I → ℝ) :
    stability t f - stability t (noise u f) =
      ∑ s, (t ^ degree s * (1 - u ^ (2 * degree s))) * coefficient f s ^ 2 := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.stability, OAI.OptimalMaxCut.Analytic.noise, OAI.OptimalMaxCut.Analytic.degree

theorem OAI.OptimalMaxCut.Analytic.stability_sub_noise_le line 113

Source documentation

A uniform multiplier bound gives a dimension-independent stability error.

theorem stability_sub_noise_le (t u η : ℝ) (f : Cube I → ℝ)
    (hf : ∀ x, -1 ≤ f x ∧ f x ≤ 1) (hη : 0 ≤ η)
    (h : ∀ j : ℕ, t ^ j * (1 - u ^ (2 * j)) ≤ η) :
    stability t f - stability t (noise u f) ≤ η := by
…

Mentions: OAI.OptimalMaxCut.Analytic.stability, OAI.OptimalMaxCut.Analytic.noise

theorem OAI.OptimalMaxCut.Analytic.walsh_zero line 125
theorem OAI.OptimalMaxCut.Analytic.degree_zero line 129
theorem OAI.OptimalMaxCut.Analytic.coefficient_one line 132
theorem OAI.OptimalMaxCut.Analytic.noise_one line 137
theorem OAI.OptimalMaxCut.Analytic.noise_mean line 143
Source documentation
Exactly preservation of the probability-normalized mean.
```
theorem noise_mean (u : ℝ) (f : Cube I → ℝ) :
    (𝔼 x, noise u f x) = 𝔼 x, f x := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.noise
lemma OAI.OptimalMaxCut.Analytic.pow_degree line 148
theorem OAI.OptimalMaxCut.Analytic.walsh_noise_kernel line 154
Source documentation
The product kernel of independent bit noise, not an assumed operator.
```
theorem walsh_noise_kernel (u : ℝ) (x y : Cube I) :
    (∑ s, u ^ degree s * walsh s x * walsh s y) =
      ∏ i, (1 + u * bitSign (x i) * bitSign (y i)) := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.degree
theorem OAI.OptimalMaxCut.Analytic.noise_kernel line 171
theorem OAI.OptimalMaxCut.Analytic.noise_kernel_mass line 189
Source documentation
Normalization of the actual bit-noise kernel, for every real multiplier.
```
theorem noise_kernel_mass (u : ℝ) (x : Cube I) :
    (𝔼 y : Cube I, ∏ i, (1 + u * bitSign (y i) * bitSign (x i))) = 1 := by
…
```

theorem OAI.OptimalMaxCut.Analytic.noise_kernel_nonneg line 196

Source documentation

The positivity restriction needed to make the kernel a probability law.

theorem noise_kernel_nonneg (u : ℝ) (hu : 0 ≤ u) (hu1 : u ≤ 1)
    (x y : Cube I) : 0 ≤ ∏ i, (1 + u * bitSign (y i) * bitSign (x i)) := by
…

theorem OAI.OptimalMaxCut.Analytic.noise_bounded line 202
theorem OAI.OptimalMaxCut.Analytic.influence_noise_le line 220
theorem OAI.OptimalMaxCut.Analytic.influence_noise_le_of_bounded line 245
Source documentation
The normalized form actually used in lem:mis.
```
theorem influence_noise_le_of_bounded (u : ℝ) (hu : 0 ≤ u) (hu1 : u ≤ 1)
    (K : ℕ) (i : I) (f : Cube I → ℝ) (hf : ∀ x, -1 ≤ f x ∧ f x ≤ 1) :
    influence i (noise u f) ≤ cutoffInfluence K i f + u ^ (2 * (K + 1)) := by
…
```
Mentions: OAI.OptimalMaxCut.Analytic.influence, OAI.OptimalMaxCut.Analytic.noise, OAI.OptimalMaxCut.Analytic.cutoffInfluence
theorem OAI.OptimalMaxCut.Analytic.nat_mul_pow_mul_one_sub_le_one line 258

theorem OAI.OptimalMaxCut.Analytic.multiplier_le line 276

Source documentation

Explicit control of the entire noise-stability multiplier sequence.

theorem multiplier_le (t u : ℝ) (ht : 0 ≤ t) (ht1 : t < 1)
    (hu : 0 ≤ u) (hu1 : u ≤ 1) (j : ℕ) :
    t ^ j * (1 - u ^ (2 * j)) ≤ 2 * (1 - u) / (1 - t) := by
…

theorem OAI.OptimalMaxCut.Analytic.exists_uniform_noise_error line 295

theorem OAI.OptimalMaxCut.Analytic.exists_influence_tail_cutoff line 312

Source documentation

Degree cutoff for the influence tail, with no dimension dependence.

theorem exists_influence_tail_cutoff (u δ : ℝ) (hu : 0 ≤ u) (hu1 : u < 1)
    (hδ : 0 < δ) : ∃ K : ℕ, 1 ≤ K ∧ u ^ (2 * (K + 1)) ≤ δ / 2 := by
…

theorem OAI.OptimalMaxCut.Analytic.uniform_noise_preparation line 322

Source documentation

All of the uniform smoothing preparation in lem:mis, independently of (the still unproved) Majority Is Stablest inequality. Both K and u precede n, and the range and centered-mean conclusions are proved from the kernel.

theorem uniform_noise_preparation (t ξ : ℝ) (ht : 0 ≤ t) (ht1 : t < 1)
    (hξ : 0 < ξ) : ∃ u : ℝ, 0 < u ∧ u < 1 ∧
      (∀ (n : ℕ) (f : Cube (Fin n) → ℝ),
        (∀ x, -1 ≤ f x ∧ f x ≤ 1) → (𝔼 x, f x) = 0 →
        (∀ x, -1 ≤ noise u f x ∧ noise u f x ≤ 1) ∧
        (𝔼 x, noise u f x) = 0 ∧
        0 ≤ stability t f - stability t (noise u f) ∧
        stability t f - stability t (noise u f) ≤ ξ / 2) ∧
      (∀ δ : ℝ, 0 < δ → ∃ K : ℕ, 1 ≤ K ∧
        ∀ (n : ℕ) (f : Cube (Fin n) → ℝ),
          (∀ x, -1 ≤ f x ∧ f x ≤ 1) →
          (∀ i, cutoffInfluence K i f < δ / 2) →
…

Mentions: OAI.OptimalMaxCut.Analytic.noise, OAI.OptimalMaxCut.Analytic.stability, OAI.OptimalMaxCut.Analytic.cutoffInfluence

def OAI.OptimalMaxCut.gwRatio line 354
def OAI.OptimalMaxCut.borellCurve line 357
lemma OAI.OptimalMaxCut.borellCurve_le line 359
lemma OAI.OptimalMaxCut.gwRatio_nonneg line 363
lemma OAI.OptimalMaxCut.gwRatio_neg_identity line 368
lemma OAI.OptimalMaxCut.gwRatio_ge_one_of_nonneg line 375
lemma OAI.OptimalMaxCut.gwRatio_neg_one line 388
lemma OAI.OptimalMaxCut.gwRatio_zero line 393
lemma OAI.OptimalMaxCut.borellCurve_half line 397
lemma OAI.OptimalMaxCut.gwRatio_neg_half line 406
theorem OAI.OptimalMaxCut.alphaGW_attained line 410
theorem OAI.OptimalMaxCut.alphaGW_pos line 454
Source documentation
Positivity of the exact attained GW constant.
```
theorem alphaGW_pos : 0 < alphaGW := by
…
```
Mentions: OAI.OptimalMaxCut.alphaGW
theorem OAI.OptimalMaxCut.exists_rational_test_correlation line 461
theorem OAI.OptimalMaxCut.exists_main_gap_parameters line 492
Source documentation
Final numerical parameter selection in the proof of thm:main. The eps below is used independently for the weighted gap and the unweighting error. The YES threshold is rational exactly, and the NO threshold is chosen strictly above the analytic upper bound and below alpha times the YES bound. This is NOT a hardness theorem or an assumed reduction.
```
theorem exists_main_gap_parameters (α : ℝ) (hα : alphaGW < α) (hα1 : α ≤ 1) :
    ∃ t ε y n : ℚ, 0 < t ∧ t < 1 ∧ 0 < ε ∧
      (ε : ℝ) < ((t : ℝ) - borellCurve t) / 4 ∧
      y = (1 + t) / 2 - 2 * ε ∧ 0 < y ∧ 0 ≤ n ∧
      (1 + borellCurve t) / 2 + 2 * ε < (n : ℝ) ∧
      (n : ℝ) < α * (y : ℝ) := by
…
```
Mentions: OAI.OptimalMaxCut.alphaGW, OAI.OptimalMaxCut.borellCurve