FourierCorrection.lean`

39 declarations, 0 contain sorry, 0 declared as axioms

Correcting an almost independent Boolean density

This is the finite Fourier correction used in the proof of the manuscript's finite-residue comparison (q:finite-law, q:fourier-correction-tv). The construction removes the chosen nonconstant Walsh coefficients and adds the constant a before normalization, retaining pointwise nonnegativity.

abbrev OAI.TwoPointCorrelations.BooleanCube line 20
def OAI.TwoPointCorrelations.cubeAverage line 23
Source documentation
Uniform average on the finite Boolean cube.
```
noncomputable def cubeAverage {n : ℕ} (f : BooleanCube n → ℝ) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.cubeAverage_add line 26
lemma OAI.TwoPointCorrelations.cubeAverage_sub line 30
lemma OAI.TwoPointCorrelations.cubeAverage_mul_const line 34
lemma OAI.TwoPointCorrelations.cubeAverage_const line 38
lemma OAI.TwoPointCorrelations.cubeAverage_sum line 42
lemma OAI.TwoPointCorrelations.cubeAverage_mono line 48
def OAI.TwoPointCorrelations.booleanSign line 53
Source documentation
The sign representation of a Boolean coordinate.
```
def booleanSign (b : Bool) : ℝ := if b then -1 else 1
```
lemma OAI.TwoPointCorrelations.booleanSign_not line 55
lemma OAI.TwoPointCorrelations.booleanSign_sq line 58
lemma OAI.TwoPointCorrelations.abs_booleanSign line 61
def OAI.TwoPointCorrelations.walsh line 65
Source documentation
The Walsh character indexed by a coordinate set.
```
def walsh {n : ℕ} (S : Finset (Fin n)) (x : BooleanCube n) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.walsh_empty line 68
lemma OAI.TwoPointCorrelations.abs_walsh line 71
lemma OAI.TwoPointCorrelations.walsh_mul_self line 75
def OAI.TwoPointCorrelations.flipBit line 82
Source documentation
The measure-preserving involution that reverses one coordinate.
```
def flipBit {n : ℕ} (i : Fin n) : BooleanCube n ≃ BooleanCube n where
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.walsh_flipBit line 96
lemma OAI.TwoPointCorrelations.cubeAverage_eq_zero_of_flip line 115
lemma OAI.TwoPointCorrelations.cubeAverage_walsh line 124
lemma OAI.TwoPointCorrelations.cubeAverage_walsh_mul line 131
def OAI.TwoPointCorrelations.lowWalshSets line 152
Source documentation
Nonempty coordinate sets through order t.
```
def lowWalshSets (n t : ℕ) : Finset (Finset (Fin n)) :=
…
```
def OAI.TwoPointCorrelations.walshCoefficient line 155
def OAI.TwoPointCorrelations.lowWalshCorrection line 158
def OAI.TwoPointCorrelations.lowWalshMass line 162
lemma OAI.TwoPointCorrelations.cubeAverage_lowWalshCorrection line 165
lemma OAI.TwoPointCorrelations.lowWalshCorrection_abs_le line 173
lemma OAI.TwoPointCorrelations.lowWalshCorrection_coefficient line 181
def OAI.TwoPointCorrelations.correctedCubeDensity line 190
Source documentation
Add a constant after removing low Walsh modes, then renormalize.
```
noncomputable def correctedCubeDensity {n : ℕ} (f : BooleanCube n → ℝ)
    (t : ℕ) (a : ℝ) (x : BooleanCube n) : ℝ :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.correctedCubeDensity_nonneg line 194
lemma OAI.TwoPointCorrelations.cubeAverage_correctedCubeDensity line 203
lemma OAI.TwoPointCorrelations.correctedCubeDensity_coefficient line 215
theorem OAI.TwoPointCorrelations.correctedCubeDensity_totalVariation_le line 231
Source documentation
Total variation from the initial density is at most 3a/2.
```
theorem correctedCubeDensity_totalVariation_le {n : ℕ} (f : BooleanCube n → ℝ)
    (t : ℕ) (a : ℝ) (hf : ∀ x, 0 ≤ f x) (hmean : cubeAverage f = 1)
    (ha : 0 ≤ a) (hmass : lowWalshMass f t ≤ a) :
    cubeAverage (fun x => |correctedCubeDensity f t a x - f x|) / 2 ≤ 3 * a / 2 := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.lowWalshMass, OAI.TwoPointCorrelations.correctedCubeDensity
def OAI.TwoPointCorrelations.cubePattern line 261
Source documentation
Indicator of a prescribed pattern on a set of coordinates.
```
noncomputable def cubePattern {n : ℕ} (S : Finset (Fin n))
    (z x : BooleanCube n) : ℝ := if ∀ i ∈ S, x i = z i then 1 else 0
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.cubePattern_walsh_expansion line 265
Source documentation
Finite Walsh inversion of a cylinder indicator.
```
lemma cubePattern_walsh_expansion {n : ℕ} (S : Finset (Fin n))
    (z x : BooleanCube n) :
    (2 : ℝ) ^ S.card * cubePattern S z x =
      ∑ T ∈ S.powerset, walsh T z * walsh T x := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubePattern, OAI.TwoPointCorrelations.walsh
lemma OAI.TwoPointCorrelations.cubeAverage_pattern_of_walsh line 300
Source documentation
Vanishing of all nonconstant Walsh coefficients on a coordinate set makes that marginal exactly uniform.
```
lemma cubeAverage_pattern_of_walsh {n : ℕ} (g : BooleanCube n → ℝ)
    (S : Finset (Fin n)) (z : BooleanCube n) (hmean : cubeAverage g = 1)
    (hcoeff : ∀ T ⊆ S, T.Nonempty → walshCoefficient g T = 0) :
    cubeAverage (fun x => g x * cubePattern S z x) = 1 / (2 : ℝ) ^ S.card := by
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.walshCoefficient, OAI.TwoPointCorrelations.cubePattern
def OAI.TwoPointCorrelations.TWiseUniformDensity line 333
Source documentation
Every assignment to at most t selected coordinates has its uniform mass.
```
def TWiseUniformDensity {n : ℕ} (g : BooleanCube n → ℝ) (t : ℕ) : Prop :=
…
```
Mentions: OAI.TwoPointCorrelations.BooleanCube
lemma OAI.TwoPointCorrelations.correctedCubeDensity_tWiseUniform line 337

theorem OAI.TwoPointCorrelations.fourierCorrection line 348

Source documentation

The complete finite correction used before applying Braverman's theorem.

theorem fourierCorrection {n : ℕ} (f : BooleanCube n → ℝ) (t : ℕ) (a : ℝ)
    (hf : ∀ x, 0 ≤ f x) (hmean : cubeAverage f = 1)
    (ha : 0 ≤ a) (hmass : lowWalshMass f t ≤ a) :
    (∀ x, 0 ≤ correctedCubeDensity f t a x) ∧
      cubeAverage (correctedCubeDensity f t a) = 1 ∧
      TWiseUniformDensity (correctedCubeDensity f t a) t ∧
      cubeAverage (fun x => |correctedCubeDensity f t a x - f x|) / 2 ≤ 3 * a / 2 :=
…

Mentions: OAI.TwoPointCorrelations.BooleanCube, OAI.TwoPointCorrelations.cubeAverage, OAI.TwoPointCorrelations.lowWalshMass, OAI.TwoPointCorrelations.correctedCubeDensity, OAI.TwoPointCorrelations.TWiseUniformDensity