Gowers-Cauchy-Schwarz and cube continuity

This file was automatically generated by Codex.

The order-three mixed cube inequality on abelian Haar probability groups, its Gowers seminorm on bounded measurable functions, and a continuous extension of the eight-input cube form to L2. The L2 estimate holds on abelian probability groups with measurable, measure-preserving inversion, including every real torus. All statements and supporting definitions use only Mathlib and this module; there are no trilinear-transform parameters. The finite-to-continuous extension uses normalized counting measure, bounded cell averages, and integer lifts of supported cubes without modular wraparound.

Verified source: blueprint/formalization_blueprint.tex, cube-definition, lines 162-175, and lem:cube-foundation, lines 216-237. The proof uses coordinate reflection, repeated Cauchy-Schwarz, and independent tetrahedral vertex coordinates, built from Mathlib Haar integration and Holder.

Haar cube averages

The Boolean parity and vertex splitting algebra below is adapted from ../lean-dfr/DFR/Auto/SmoothingIneq3D/Smoothing3D.lean, copyright 2026 Joris Roos, Apache 2.0. Here parity counts true coordinates, exactly as in the supplied blueprint.

noncomputable def TrilinearHT.Auto.cubeConj (n : ℕ) (z : ℂ) : ℂ

Conjugation to the power of a natural number, reduced modulo two.

Equations

• TrilinearHT.Auto.cubeConj n z = if Even n then z else (starRingEnd ℂ) z

theorem TrilinearHT.Auto.cubeConj_succ (n : ℕ) (z : ℂ) : cubeConj (n + 1) z = (starRingEnd ℂ) (cubeConj n z)

theorem TrilinearHT.Auto.norm_cubeConj (n : ℕ) (z : ℂ) : ‖cubeConj n z‖ = ‖z‖

def TrilinearHT.Auto.cubeWeight {j : ℕ} (ω : Fin j → Bool) : ℕ

Hamming weight of a Boolean cube vertex.

Equations

• TrilinearHT.Auto.cubeWeight ω = ∑ i : Fin j, if ω i = true then 1 else 0

def TrilinearHT.Auto.cubeShift {G : Type u_1} [AddCommMonoid G] {j : ℕ} (h : Fin j → G) (ω : Fin j → Bool) : G

The group-valued shift ω · h at a cube vertex.

Equations

• TrilinearHT.Auto.cubeShift h ω = ∑ i : Fin j, if ω i = true then h i else 0

theorem TrilinearHT.Auto.cubeWeight_cons {j : ℕ} (b : Bool) (ω : Fin j → Bool) : cubeWeight (Fin.cons b ω) = (if b = true then 1 else 0) + cubeWeight ω

theorem TrilinearHT.Auto.cubeShift_cons {G : Type u_1} [AddCommMonoid G] {j : ℕ} (h : Fin (j + 1) → G) (b : Bool) (ω : Fin j → Bool) : cubeShift h (Fin.cons b ω) = (if b = true then h 0 else 0) + cubeShift (fun (i : Fin j) => h i.succ) ω

def TrilinearHT.Auto.cubeConsEquiv (j : ℕ) : Bool × (Fin j → Bool) ≃ (Fin (j + 1) → Bool)

Splitting a Boolean vertex into its first coordinate and its remaining face.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.cubeIntegrand {G : Type u_1} [AddCommMonoid G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) (h : Fin j → G) (x : G) : ℂ

The literal mixed cube integrand in blueprint cube-definition.

Equations

• TrilinearHT.Auto.cubeIntegrand f h x = ∏ ω : Fin j → Bool, TrilinearHT.Auto.cubeConj (TrilinearHT.Auto.cubeWeight ω) (f ω (x + TrilinearHT.Auto.cubeShift h ω))

noncomputable def TrilinearHT.Auto.cubeAverage {G : Type u_1} [AddCommMonoid G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (j : ℕ) (f : (Fin j → Bool) → G → ℂ) : ℂ

The mixed Gowers cube average with probability measure on every variable.

Equations

• TrilinearHT.Auto.cubeAverage μ j f = ∫ (h : Fin j → G), ∫ (x : G), TrilinearHT.Auto.cubeIntegrand f h x ∂μ ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ

noncomputable def TrilinearHT.Auto.diagonalCubeIntegrand {G : Type u_1} [AddCommMonoid G] (j : ℕ) (f : G → ℂ) (h : Fin j → G) (x : G) : ℂ

The diagonal cube integrand, before taking a nonnegative root.

Equations

• TrilinearHT.Auto.diagonalCubeIntegrand j f h x = TrilinearHT.Auto.cubeIntegrand (fun (x : Fin j → Bool) => f) h x

theorem TrilinearHT.Auto.diagonalCubeIntegrand_zero {G : Type u_1} [AddCommMonoid G] (f : G → ℂ) (h : Fin 0 → G) (x : G) : diagonalCubeIntegrand 0 f h x = f x

theorem TrilinearHT.Auto.diagonalCubeIntegrand_succ {G : Type u_1} [AddCommMonoid G] (j : ℕ) (f : G → ℂ) (h : Fin (j + 1) → G) (x : G) : diagonalCubeIntegrand (j + 1) f h x = diagonalCubeIntegrand j f (fun (i : Fin j) => h i.succ) x * (starRingEnd ℂ) (diagonalCubeIntegrand j f (fun (i : Fin j) => h i.succ) (x + h 0))

Separating one increment gives the product of a face and its conjugate translate.

theorem TrilinearHT.Auto.measurable_cubeConj (n : ℕ) : Measurable (cubeConj n)

theorem TrilinearHT.Auto.measurable_cubeShift {G : Type u_1} [AddCommMonoid G] [MeasurableSpace G] [MeasurableAdd₂ G] {j : ℕ} (ω : Fin j → Bool) : Measurable fun (h : Fin j → G) => cubeShift h ω

theorem TrilinearHT.Auto.measurable_cubeIntegrand {G : Type u_1} [AddCommMonoid G] [MeasurableSpace G] [MeasurableAdd₂ G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) (hf : ∀ (ω : Fin j → Bool), Measurable (f ω)) : Measurable fun (p : (Fin j → G) × G) => cubeIntegrand f p.1 p.2

theorem TrilinearHT.Auto.norm_cubeIntegrand_le {G : Type u_1} [AddCommMonoid G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) {M : ℝ} (hf : ∀ (ω : Fin j → Bool) (x : G), ‖f ω x‖ ≤ M) (h : Fin j → G) (x : G) : ‖cubeIntegrand f h x‖ ≤ M ^ 2 ^ j

theorem TrilinearHT.Auto.integrable_of_measurable_bounded {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {f : X → ℂ} (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : X), ‖f x‖ ≤ M) : MeasureTheory.Integrable f μ

A bounded measurable complex function on a finite measure space is integrable.

theorem TrilinearHT.Auto.integral_haar_correlation {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : ∫ (h : G), ∫ (x : G), f x * (starRingEnd ℂ) (f (x + h)) ∂μ ∂μ = ↑(‖∫ (x : G), f x ∂μ‖ ^ 2)

Haar independence of a point and its independent translate.

theorem TrilinearHT.Auto.integral_pi_cons {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {j : ℕ} (F : (Fin (j + 1) → G) → ℂ) (hF : Measurable F) {M : ℝ} (hbound : ∀ (h : Fin (j + 1) → G), ‖F h‖ ≤ M) : (∫ (h : Fin (j + 1) → G), F h ∂MeasureTheory.Measure.pi fun (x : Fin (j + 1)) => μ) = ∫ (h : Fin j → G), ∫ (t : G), F (Fin.cons t h) ∂μ ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ

Fubini splitting of the first coordinate of a finite probability product.

theorem TrilinearHT.Auto.cubeAverage_diagonal_eq_integral_sq {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : (cubeAverage μ (j + 1) fun (x : Fin (j + 1) → Bool) => f) = ↑(∫ (h : Fin j → G), ‖∫ (x : G), diagonalCubeIntegrand j f h x ∂μ‖ ^ 2 ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ)

Blueprint cube-definition, lines 168–172: the diagonal cube average is the average of squared absolute face averages. This proves both reality and positivity.

theorem TrilinearHT.Auto.cubeAverage_diagonal_im_eq_zero {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : (cubeAverage μ j fun (x : Fin j → Bool) => f).im = 0

Reality of every positive-order diagonal Haar cube average.

theorem TrilinearHT.Auto.cubeAverage_diagonal_re_nonneg {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : 0 ≤ (cubeAverage μ j fun (x : Fin j → Bool) => f).re

Nonnegativity of every positive-order diagonal Haar cube average.

noncomputable def TrilinearHT.Auto.gowersNorm {G : Type u_1} [AddCommMonoid G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (j : ℕ) (f : G → ℂ) : ℝ

Blueprint cube-definition, line 174: the nonnegative 2^j-th root of the diagonal cube average. Its positivity and root identity hold for j ≥ 1.

Equations

• TrilinearHT.Auto.gowersNorm μ j f = (TrilinearHT.Auto.cubeAverage μ j fun (x : Fin j → Bool) => f).re ^ (↑(2 ^ j))⁻¹

theorem TrilinearHT.Auto.gowersNorm_nonneg {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : 0 ≤ gowersNorm μ j f

theorem TrilinearHT.Auto.gowersNorm_pow {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : gowersNorm μ j f ^ 2 ^ j = (cubeAverage μ j fun (x : Fin j → Bool) => f).re

theorem TrilinearHT.Auto.cubeConj_mul (n : ℕ) (a b : ℂ) : cubeConj n (a * b) = cubeConj n a * cubeConj n b

theorem TrilinearHT.Auto.cubeConj_conj (n : ℕ) (a : ℂ) : cubeConj n ((starRingEnd ℂ) a) = (starRingEnd ℂ) (cubeConj n a)

theorem TrilinearHT.Auto.diagonalCubeIntegrand_mul {G : Type u_1} [AddCommGroup G] (j : ℕ) (f g : G → ℂ) (h : Fin j → G) (x : G) : diagonalCubeIntegrand j (fun (x : G) => f x * g x) h x = diagonalCubeIntegrand j f h x * diagonalCubeIntegrand j g h x

theorem TrilinearHT.Auto.diagonalCubeIntegrand_conj {G : Type u_1} [AddCommGroup G] (j : ℕ) (f : G → ℂ) (h : Fin j → G) (x : G) : diagonalCubeIntegrand j (fun (x : G) => (starRingEnd ℂ) (f x)) h x = (starRingEnd ℂ) (diagonalCubeIntegrand j f h x)

theorem TrilinearHT.Auto.diagonalCubeIntegrand_translate {G : Type u_1} [AddCommGroup G] (j : ℕ) (f : G → ℂ) (h : Fin j → G) (x t : G) : diagonalCubeIntegrand j (fun (y : G) => f (y + t)) h x = diagonalCubeIntegrand j f h (x + t)

Coordinate reflection for the Haar cube Cauchy–Schwarz inequality.

def TrilinearHT.Auto.cubeFace {j : ℕ} {E : Type u_1} (i : Fin (j + 1)) (b : Bool) (f : (Fin (j + 1) → Bool) → E) : (Fin j → Bool) → E

Restrict a cube-indexed family to the face with coordinate i fixed to b.

Equations

• TrilinearHT.Auto.cubeFace i b f ω = f (i.insertNth b ω)

def TrilinearHT.Auto.cubeCopy {j : ℕ} {E : Type u_1} (i : Fin j) (b : Bool) (f : (Fin j → Bool) → E) : (Fin j → Bool) → E

Copy the face with coordinate i fixed to b onto the full cube.

Equations

• TrilinearHT.Auto.cubeCopy i b f ω = f (Function.update ω i b)

theorem TrilinearHT.Auto.cubeWeight_insertNth {j : ℕ} (i : Fin (j + 1)) (b : Bool) (ω : Fin j → Bool) : cubeWeight (i.insertNth b ω) = (if b = true then 1 else 0) + cubeWeight ω

theorem TrilinearHT.Auto.cubeShift_insertNth {G : Type u_1} [AddCommMonoid G] {j : ℕ} (i : Fin (j + 1)) (h : Fin (j + 1) → G) (b : Bool) (ω : Fin j → Bool) : cubeShift h (i.insertNth b ω) = (if b = true then h i else 0) + cubeShift (fun (k : Fin j) => h (i.succAbove k)) ω

theorem TrilinearHT.Auto.cubeIntegrand_split {G : Type u_1} [AddCommMonoid G] {j : ℕ} (i : Fin (j + 1)) (f : (Fin (j + 1) → Bool) → G → ℂ) (h : Fin j → G) (t x : G) : cubeIntegrand f (i.insertNth t h) x = cubeIntegrand (cubeFace i false f) h x * (starRingEnd ℂ) (cubeIntegrand (cubeFace i true f) h (x + t))

theorem TrilinearHT.Auto.integral_pi_insertNth {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {j : ℕ} (i : Fin (j + 1)) (F : (Fin (j + 1) → G) → ℂ) (hF : Measurable F) {M : ℝ} (hbound : ∀ (h : Fin (j + 1) → G), ‖F h‖ ≤ M) : (∫ (h : Fin (j + 1) → G), F h ∂MeasureTheory.Measure.pi fun (x : Fin (j + 1)) => μ) = ∫ (h : Fin j → G), ∫ (t : G), F (i.insertNth t h) ∂μ ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ

theorem TrilinearHT.Auto.integral_haar_cross_correlation {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) {M N : ℝ} (hboundf : ∀ (x : G), ‖f x‖ ≤ M) (hboundg : ∀ (x : G), ‖g x‖ ≤ N) : ∫ (h : G), ∫ (x : G), f x * (starRingEnd ℂ) (g (x + h)) ∂μ ∂μ = (∫ (x : G), f x ∂μ) * (starRingEnd ℂ) (∫ (x : G), g x ∂μ)

theorem TrilinearHT.Auto.cubeAverage_split {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (i : Fin (j + 1)) (f : (Fin (j + 1) → Bool) → G → ℂ) (hf : ∀ (ω : Fin (j + 1) → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin (j + 1) → Bool) (x : G), ‖f ω x‖ ≤ M) : cubeAverage μ (j + 1) f = ∫ (h : Fin j → G), (∫ (x : G), cubeIntegrand (cubeFace i false f) h x ∂μ) * (starRingEnd ℂ) (∫ (x : G), cubeIntegrand (cubeFace i true f) h x ∂μ) ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ

Every coordinate splitting expresses a mixed cube as an inner product of face averages.

theorem TrilinearHT.Auto.norm_integral_mul_conj_sq_le {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] (f g : X → ℂ) (hf : Measurable f) (hg : Measurable g) {M N : ℝ} (hbf : ∀ (x : X), ‖f x‖ ≤ M) (hbg : ∀ (x : X), ‖g x‖ ≤ N) : ‖∫ (x : X), f x * (starRingEnd ℂ) (g x) ∂μ‖ ^ 2 ≤ (∫ (x : X), ‖f x‖ ^ 2 ∂μ) * ∫ (x : X), ‖g x‖ ^ 2 ∂μ

theorem TrilinearHT.Auto.cubeFace_copy {j : ℕ} {E : Type u_1} (i : Fin (j + 1)) (b c : Bool) (f : (Fin (j + 1) → Bool) → E) : cubeFace i c (cubeCopy i b f) = cubeFace i b f

theorem TrilinearHT.Auto.cubeAverage_copy_eq_sq {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (i : Fin (j + 1)) (b : Bool) (f : (Fin (j + 1) → Bool) → G → ℂ) (hf : ∀ (ω : Fin (j + 1) → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin (j + 1) → Bool) (x : G), ‖f ω x‖ ≤ M) : cubeAverage μ (j + 1) (cubeCopy i b f) = ↑(∫ (h : Fin j → G), ‖∫ (x : G), cubeIntegrand (cubeFace i b f) h x ∂μ‖ ^ 2 ∂MeasureTheory.Measure.pi fun (x : Fin j) => μ)

The two reflected cubes are squares of face averages, hence real and nonnegative.

theorem TrilinearHT.Auto.cubeAverage_copy_re_nonneg {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (i : Fin (j + 1)) (b : Bool) (f : (Fin (j + 1) → Bool) → G → ℂ) (hf : ∀ (ω : Fin (j + 1) → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin (j + 1) → Bool) (x : G), ‖f ω x‖ ≤ M) : 0 ≤ (cubeAverage μ (j + 1) (cubeCopy i b f)).re

theorem TrilinearHT.Auto.cubeAverage_coordinate_cs {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (i : Fin (j + 1)) (f : (Fin (j + 1) → Bool) → G → ℂ) (hf : ∀ (ω : Fin (j + 1) → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin (j + 1) → Bool) (x : G), ‖f ω x‖ ≤ M) : ‖cubeAverage μ (j + 1) f‖ ^ 2 ≤ (cubeAverage μ (j + 1) (cubeCopy i false f)).re * (cubeAverage μ (j + 1) (cubeCopy i true f)).re

One coordinate-reflection Cauchy–Schwarz step from lem:cube-foundation.

def TrilinearHT.Auto.cubeReflections {d : ℕ} {E : Type u_1} (n : ℕ) : (Fin n → Fin d) → (Fin n → Bool) → ((Fin d → Bool) → E) → (Fin d → Bool) → E

Apply the specified coordinate reflections in order.

Equations

• TrilinearHT.Auto.cubeReflections 0 x_4 x_5 x✝ = x✝
• TrilinearHT.Auto.cubeReflections n.succ c ω x✝ = TrilinearHT.Auto.cubeReflections n (fun (i : Fin n) => c i.succ) (fun (i : Fin n) => ω i.succ) (TrilinearHT.Auto.cubeCopy (c 0) (ω 0) x✝)

theorem TrilinearHT.Auto.cube_reflection_iteration {d : ℕ} {E : Type u_1} (P : ((Fin d → Bool) → E) → Prop) (Q : ((Fin d → Bool) → E) → ℝ) (hQ : ∀ (f : (Fin d → Bool) → E), P f → 0 ≤ Q f) (hcopy : ∀ (i : Fin d) (b : Bool) (f : (Fin d → Bool) → E), P f → P (cubeCopy i b f)) (hcs : ∀ (i : Fin d) (f : (Fin d → Bool) → E), P f → Q f ^ 2 ≤ Q (cubeCopy i false f) * Q (cubeCopy i true f)) (n : ℕ) (c : Fin n → Fin d) (f : (Fin d → Bool) → E) (hf : P f) : Q f ^ 2 ^ n ≤ ∏ ω : Fin n → Bool, Q (cubeReflections n c ω f)

The finite Cauchy–Schwarz iteration, restricted to any class closed under reflections.

theorem TrilinearHT.Auto.cubeReflections_three {E : Type u_1} (ω : Fin 3 → Bool) (f : (Fin 3 → Bool) → E) : cubeReflections 3 id ω f = fun (x : Fin 3 → Bool) => f ω

theorem TrilinearHT.Auto.cubeAverage_diagonal_norm_eq_re {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {j : ℕ} (hj : 1 ≤ j) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbound : ∀ (x : G), ‖f x‖ ≤ M) : ‖cubeAverage μ j fun (x : Fin j → Bool) => f‖ = (cubeAverage μ j fun (x : Fin j → Bool) => f).re

theorem TrilinearHT.Auto.cubeAverage_three_cs_pow {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin 3 → Bool) (x : G), ‖f ω x‖ ≤ M) : ‖cubeAverage μ 3 f‖ ^ 8 ≤ ∏ ω : Fin 3 → Bool, (cubeAverage μ 3 fun (x : Fin 3 → Bool) => f ω).re

The eightfold reflection estimate before taking nonnegative eighth roots.

theorem TrilinearHT.Auto.cubeAverage_three_cs {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) {M : ℝ} (hbound : ∀ (ω : Fin 3 → Bool) (x : G), ‖f ω x‖ ≤ M) : ‖cubeAverage μ 3 f‖ ≤ ∏ ω : Fin 3 → Bool, gowersNorm μ 3 (f ω)

Blueprint lem:cube-foundation: mixed Gowers–Cauchy–Schwarz on Haar probability groups.

theorem TrilinearHT.Auto.cubeConj_add (n : ℕ) (a b : ℂ) : cubeConj n (a + b) = cubeConj n a + cubeConj n b

def TrilinearHT.Auto.cubeChoice {G : Type u_1} {j : ℕ} (f g : G → ℂ) (σ : (Fin j → Bool) → Bool) : (Fin j → Bool) → G → ℂ

Choose either f or g independently at each cube vertex.

Equations

• TrilinearHT.Auto.cubeChoice f g σ ω = if σ ω = true then f else g

theorem TrilinearHT.Auto.cubeIntegrand_add_expansion {G : Type u_1} [AddCommGroup G] (j : ℕ) (f g : G → ℂ) (h : Fin j → G) (x : G) : cubeIntegrand (fun (x : Fin j → Bool) (x_1 : G) => f x_1 + g x_1) h x = ∑ σ : (Fin j → Bool) → Bool, cubeIntegrand (cubeChoice f g σ) h x

theorem TrilinearHT.Auto.measurable_cubeChoice {G : Type u_1} [MeasurableSpace G] {j : ℕ} (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) (σ : (Fin j → Bool) → Bool) (ω : Fin j → Bool) : Measurable (cubeChoice f g σ ω)

theorem TrilinearHT.Auto.norm_cubeChoice_le {G : Type u_1} {j : ℕ} (f g : G → ℂ) {M : ℝ} (hf : ∀ (x : G), ‖f x‖ ≤ M) (hg : ∀ (x : G), ‖g x‖ ≤ M) (σ : (Fin j → Bool) → Bool) (ω : Fin j → Bool) (x : G) : ‖cubeChoice f g σ ω x‖ ≤ M

theorem TrilinearHT.Auto.cubeIntegrand_integrable {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {j : ℕ} (u : (Fin j → Bool) → G → ℂ) (hu : ∀ (ω : Fin j → Bool), Measurable (u ω)) {M : ℝ} (hbu : ∀ (ω : Fin j → Bool) (x : G), ‖u ω x‖ ≤ M) (h : Fin j → G) : MeasureTheory.Integrable (cubeIntegrand u h) μ

theorem TrilinearHT.Auto.cubeChoice_integrable {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] (j : ℕ) (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) {M : ℝ} (hbf : ∀ (x : G), ‖f x‖ ≤ M) (hbg : ∀ (x : G), ‖g x‖ ≤ M) (σ : (Fin j → Bool) → Bool) (h : Fin j → G) : MeasureTheory.Integrable (cubeIntegrand (cubeChoice f g σ) h) μ

theorem TrilinearHT.Auto.cubeChoice_integral_integrable {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] (j : ℕ) (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) {M : ℝ} (hbf : ∀ (x : G), ‖f x‖ ≤ M) (hbg : ∀ (x : G), ‖g x‖ ≤ M) (σ : (Fin j → Bool) → Bool) : MeasureTheory.Integrable (fun (h : Fin j → G) => ∫ (x : G), cubeIntegrand (cubeChoice f g σ) h x ∂μ) (MeasureTheory.Measure.pi fun (x : Fin j) => μ)

theorem TrilinearHT.Auto.cubeAverage_add_expansion {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] (j : ℕ) (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) {M : ℝ} (hbf : ∀ (x : G), ‖f x‖ ≤ M) (hbg : ∀ (x : G), ‖g x‖ ≤ M) : (cubeAverage μ j fun (x : Fin j → Bool) (x_1 : G) => f x_1 + g x_1) = ∑ σ : (Fin j → Bool) → Bool, cubeAverage μ j (cubeChoice f g σ)

theorem TrilinearHT.Auto.sum_cubeChoice_products {j : ℕ} (a b : ℝ) : (∑ σ : (Fin j → Bool) → Bool, ∏ ω : Fin j → Bool, if σ ω = true then a else b) = (a + b) ^ 2 ^ j

theorem TrilinearHT.Auto.gowersNorm_three_add_le {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) {M : ℝ} (hbf : ∀ (x : G), ‖f x‖ ≤ M) (hbg : ∀ (x : G), ‖g x‖ ≤ M) : (gowersNorm μ 3 fun (x : G) => f x + g x) ≤ gowersNorm μ 3 f + gowersNorm μ 3 g

The triangle inequality for the order-three Haar Gowers seminorm on bounded measurable inputs.

theorem TrilinearHT.Auto.diagonalCubeIntegrand_const_three {G : Type u_1} [AddCommGroup G] (c : ℂ) (h : Fin 3 → G) (x : G) : diagonalCubeIntegrand 3 (fun (x : G) => c) h x = ↑‖c‖ ^ 8

theorem TrilinearHT.Auto.cubeAverage_three_const_mul {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (c : ℂ) (f : G → ℂ) : (cubeAverage μ 3 fun (x : Fin 3 → Bool) (x_1 : G) => c * f x_1) = ↑‖c‖ ^ 8 * cubeAverage μ 3 fun (x : Fin 3 → Bool) => f

theorem TrilinearHT.Auto.gowersNorm_three_const_mul {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (c : ℂ) (f : G → ℂ) (hf : Measurable f) {M : ℝ} (hbf : ∀ (x : G), ‖f x‖ ≤ M) : (gowersNorm μ 3 fun (x : G) => c * f x) = ‖c‖ * gowersNorm μ 3 f

Absolute homogeneity of the order-three Haar Gowers seminorm.

Independent tetrahedral vertex coordinates for the cube L² estimate.

def TrilinearHT.Auto.tetrahedronShear {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (j : ℕ) : G × (Fin j → G) ≃ᵐ G × (Fin j → G)

Measurable change from a base point and increments to independent vertex coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.measurePreserving_tetrahedronShear {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) : MeasureTheory.MeasurePreserving (⇑(tetrahedronShear j)) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ)) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ))

theorem TrilinearHT.Auto.integral_tetrahedron_product {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) (f : G → ℝ) (g : Fin j → G → ℝ) : ∫ (p : G × (Fin j → G)), f p.1 * ∏ i : Fin j, g i (p.1 + p.2 i) ∂μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ) = (∫ (x : G), f x ∂μ) * ∏ i : Fin j, ∫ (x : G), g i x ∂μ

The base vertex and its three edge neighbors have independent Haar distributions.

def TrilinearHT.Auto.cubeOpposite {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (j : ℕ) : G × (Fin j → G) ≃ᵐ G × (Fin j → G)

Measure-coordinate involution exchanging opposite cube vertices.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.measurePreserving_cubeOpposite {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (j : ℕ) : MeasureTheory.MeasurePreserving (⇑(cubeOpposite j)) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ)) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ))

theorem TrilinearHT.Auto.integral_opposite_tetrahedron_product {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (j : ℕ) (f : G → ℝ) (g : Fin j → G → ℝ) : ∫ (p : G × (Fin j → G)), f (p.1 + ∑ i : Fin j, p.2 i) * ∏ i : Fin j, g i (p.1 + ∑ k : Fin j, p.2 k - p.2 i) ∂μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ) = (∫ (x : G), f x ∂μ) * ∏ i : Fin j, ∫ (x : G), g i x ∂μ

The opposite vertex and its three edge neighbors also have independent Haar distributions.

def TrilinearHT.Auto.cubeUnitVertex (i : Fin 3) : Fin 3 → Bool

The cube vertex with only coordinate i set to true.

Equations

• TrilinearHT.Auto.cubeUnitVertex i = ![![true, false, false], ![false, true, false], ![false, false, true]] i

def TrilinearHT.Auto.cubeCoUnitVertex (i : Fin 3) : Fin 3 → Bool

The cube vertex with only coordinate i set to false.

Equations

• TrilinearHT.Auto.cubeCoUnitVertex i = ![![false, true, true], ![true, false, true], ![true, true, false]] i

theorem TrilinearHT.Auto.prod_boolCube_succ {R : Type u_1} [CommMonoid R] (j : ℕ) (F : (Fin (j + 1) → Bool) → R) : ∏ ω : Fin (j + 1) → Bool, F ω = (∏ ω : Fin j → Bool, F (Fin.cons false ω)) * ∏ ω : Fin j → Bool, F (Fin.cons true ω)

theorem TrilinearHT.Auto.cube_vertex_product_three {G : Type u_1} {R : Type u_2} [AddCommGroup G] [CommRing R] (F : (Fin 3 → Bool) → G → R) (h : Fin 3 → G) (x : G) : ∏ ω : Fin 3 → Bool, F ω (x + cubeShift h ω) = (F ![false, false, false] x * ∏ i : Fin 3, F (cubeUnitVertex i) (x + h i)) * (F ![true, true, true] (x + ∑ i : Fin 3, h i) * ∏ i : Fin 3, F (cubeCoUnitVertex i) (x + ∑ k : Fin 3, h k - h i))

theorem TrilinearHT.Auto.memLp_tetrahedron_product {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) (f : G → ℝ) (g : Fin j → G → ℝ) (hf : Measurable f) (hg : ∀ (i : Fin j), Measurable (g i)) (hfl : MeasureTheory.MemLp f 2 μ) (hgl : ∀ (i : Fin j), MeasureTheory.MemLp (g i) 2 μ) : MeasureTheory.MemLp (fun (p : G × (Fin j → G)) => f p.1 * ∏ i : Fin j, g i (p.1 + p.2 i)) 2 (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ))

Products of independent L² factors remain in L² on the product probability space.

theorem TrilinearHT.Auto.prod_cube_vertices_three {R : Type u_1} [CommRing R] (F : (Fin 3 → Bool) → R) : ∏ ω : Fin 3 → Bool, F ω = (F ![false, false, false] * ∏ i : Fin 3, F (cubeUnitVertex i)) * (F ![true, true, true] * ∏ i : Fin 3, F (cubeCoUnitVertex i))

theorem TrilinearHT.Auto.cubeIntegrand_three_integrable {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) (hfl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (f ω) 2 μ) : MeasureTheory.Integrable (fun (p : G × (Fin 3 → G)) => cubeIntegrand f p.2 p.1) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin 3) => μ))

The full cube integrand is integrable for eight measurable L² inputs.

noncomputable def TrilinearHT.Auto.haarL2Norm {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : G → ℂ) : ℝ

Square root of the integral of the squared norm with respect to μ.

Equations

• TrilinearHT.Auto.haarL2Norm μ f = √(∫ (x : G), ‖f x‖ ^ 2 ∂μ)

theorem TrilinearHT.Auto.haarL2Norm_sq {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : G → ℂ) : haarL2Norm μ f ^ 2 = ∫ (x : G), ‖f x‖ ^ 2 ∂μ

theorem TrilinearHT.Auto.cubeAverage_three_le_L2 {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) (hfl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (f ω) 2 μ) : ‖cubeAverage μ 3 f‖ ≤ ∏ ω : Fin 3 → Bool, haarL2Norm μ (f ω)

Blueprint eq:cube-L2, in the stronger form valid on any abelian Haar probability group with measurable inversion: all eight measurable inputs may already lie in L².

theorem TrilinearHT.Auto.measurePreserving_cubeVertex {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) (ω : Fin j → Bool) : MeasureTheory.MeasurePreserving (fun (p : G × (Fin j → G)) => p.1 + cubeShift p.2 ω) (μ.prod (MeasureTheory.Measure.pi fun (x : Fin j) => μ)) μ

theorem TrilinearHT.Auto.cubeAverage_three_congr_ae {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f g : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) (hg : ∀ (ω : Fin 3 → Bool), Measurable (g ω)) (hfl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (f ω) 2 μ) (hgl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (g ω) 2 μ) (heq : ∀ (ω : Fin 3 → Bool), f ω =ᵐ[μ] g ω) : cubeAverage μ 3 f = cubeAverage μ 3 g

noncomputable def TrilinearHT.Auto.l2Representative {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : G → ℂ

A measurable representative is used only to evaluate integrals; the cube form below is independent of this choice by cubeAverage_three_congr_ae.

Equations

• TrilinearHT.Auto.l2Representative μ f = MeasureTheory.AEStronglyMeasurable.mk ↑↑f ⋯

theorem TrilinearHT.Auto.l2Representative_measurable {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : Measurable (l2Representative μ f)

theorem TrilinearHT.Auto.l2Representative_ae {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : l2Representative μ f =ᵐ[μ] ↑↑f

theorem TrilinearHT.Auto.l2Representative_memLp {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : MeasureTheory.MemLp (l2Representative μ f) 2 μ

theorem TrilinearHT.Auto.haarL2Norm_l2Representative {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : haarL2Norm μ (l2Representative μ f) = ‖f‖

theorem TrilinearHT.Auto.cubeIntegrand_update {G : Type u_1} [AddCommGroup G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) (ω : Fin j → Bool) (g : G → ℂ) (h : Fin j → G) (x : G) : cubeIntegrand (Function.update f ω g) h x = cubeConj (cubeWeight ω) (g (x + cubeShift h ω)) * ∏ v ∈ Finset.univ.erase ω, cubeConj (cubeWeight v) (f v (x + cubeShift h v))

theorem TrilinearHT.Auto.cubeConj_real_smul (n : ℕ) (r : ℝ) (z : ℂ) : cubeConj n (r • z) = r • cubeConj n z

theorem TrilinearHT.Auto.cubeIntegrand_update_add {G : Type u_1} [AddCommGroup G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) (ω : Fin j → Bool) (g k : G → ℂ) (h : Fin j → G) (x : G) : cubeIntegrand (Function.update f ω (g + k)) h x = cubeIntegrand (Function.update f ω g) h x + cubeIntegrand (Function.update f ω k) h x

theorem TrilinearHT.Auto.cubeIntegrand_update_smul {G : Type u_1} [AddCommGroup G] {j : ℕ} (f : (Fin j → Bool) → G → ℂ) (ω : Fin j → Bool) (r : ℝ) (g : G → ℂ) (h : Fin j → G) (x : G) : cubeIntegrand (Function.update f ω (r • g)) h x = r • cubeIntegrand (Function.update f ω g) h x

theorem TrilinearHT.Auto.cubeAverage_three_update_add {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) (hfl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (f ω) 2 μ) (ω : Fin 3 → Bool) (g k : G → ℂ) (hg : Measurable g) (hk : Measurable k) (hgl : MeasureTheory.MemLp g 2 μ) (hkl : MeasureTheory.MemLp k 2 μ) : cubeAverage μ 3 (Function.update f ω (g + k)) = cubeAverage μ 3 (Function.update f ω g) + cubeAverage μ 3 (Function.update f ω k)

theorem TrilinearHT.Auto.cubeAverage_three_update_smul {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : (Fin 3 → Bool) → G → ℂ) (ω : Fin 3 → Bool) (r : ℝ) (g : G → ℂ) : cubeAverage μ 3 (Function.update f ω (r • g)) = r • cubeAverage μ 3 (Function.update f ω g)

noncomputable def TrilinearHT.Auto.l2CubeAverage {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : (Fin 3 → Bool) → ↥(MeasureTheory.Lp ℂ 2 μ)) : ℂ

Cube average computed from the chosen representatives of eight L² classes.

Equations

• TrilinearHT.Auto.l2CubeAverage μ f = TrilinearHT.Auto.cubeAverage μ 3 fun (ω : Fin 3 → Bool) => TrilinearHT.Auto.l2Representative μ (f ω)

theorem TrilinearHT.Auto.l2CubeAverage_update_eq {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : (Fin 3 → Bool) → ↥(MeasureTheory.Lp ℂ 2 μ)) (ω : Fin 3 → Bool) (u : ↥(MeasureTheory.Lp ℂ 2 μ)) (g : G → ℂ) (hg : Measurable g) (hgl : MeasureTheory.MemLp g 2 μ) (hgu : g =ᵐ[μ] ↑↑u) : l2CubeAverage μ (Function.update f ω u) = cubeAverage μ 3 (Function.update (fun (v : Fin 3 → Bool) => l2Representative μ (f v)) ω g)

noncomputable def TrilinearHT.Auto.l2CubeMultilinear {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : MultilinearMap ℝ (fun (x : Fin 3 → Bool) => ↥(MeasureTheory.Lp ℂ 2 μ)) ℂ

The cube form is real multilinear: odd vertices conjugate their complex input.

Equations

• TrilinearHT.Auto.l2CubeMultilinear μ = MultilinearMap.mk' (TrilinearHT.Auto.l2CubeAverage μ) ⋯ ⋯

noncomputable def TrilinearHT.Auto.l2CubeContinuous {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : ContinuousMultilinearMap ℝ (fun (x : Fin 3 → Bool) => ↥(MeasureTheory.Lp ℂ 2 μ)) ℂ

Blueprint lem:cube-foundation: the continuous extension to eight L² inputs.

Equations

• TrilinearHT.Auto.l2CubeContinuous μ = (TrilinearHT.Auto.l2CubeMultilinear μ).mkContinuous 1 ⋯

noncomputable def TrilinearHT.Auto.finiteHaar (G : Type u_1) [Fintype G] [MeasurableSpace G] : MeasureTheory.Measure G

Normalized counting measure, the Haar probability measure on a finite group.

Equations

• TrilinearHT.Auto.finiteHaar G = (↑(Fintype.card G))⁻¹ • MeasureTheory.Measure.count

instance TrilinearHT.Auto.finiteHaar_isProbabilityMeasure (G : Type u_1) [Fintype G] [Nonempty G] [MeasurableSpace G] : MeasureTheory.IsProbabilityMeasure (finiteHaar G)

instance TrilinearHT.Auto.finiteHaar_isAddLeftInvariant (G : Type u_1) [AddGroup G] [Fintype G] [MeasurableSpace G] [MeasurableAdd G] : (finiteHaar G).IsAddLeftInvariant

noncomputable def TrilinearHT.Auto.cyclicCellAverage (L : ℕ) (g : ℝ → ℂ) (j : ZMod (16 * L + 1)) : ℂ

Normalized cell average on the first L cells of the cyclic group, extended by zero.

Equations

• TrilinearHT.Auto.cyclicCellAverage L g j = if j.val < L then ↑L * ∫ (x : ℝ) in ↑j.val / ↑L..(↑j.val + 1) / ↑L, g x else 0

theorem TrilinearHT.Auto.cyclicCellAverage_norm_le_one {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hg : ∀ (x : ℝ), ‖g x‖ ≤ 1) (j : ZMod (16 * L + 1)) : ‖cyclicCellAverage L g j‖ ≤ 1

theorem TrilinearHT.Auto.cyclic_cube_no_wrap (L : ℕ) (x j : ℤ) (hxlo : -3 * ↑L ≤ x) (hxhi : x ≤ 4 * ↑L) (hj0 : 0 ≤ j) (hjL : j < ↑L) : ↑x = ↑j ↔ x = j

theorem TrilinearHT.Auto.integer_cube_vertex_bounds {d : ℕ} {L x : ℤ} (hL : 0 ≤ L) (hx0 : 0 ≤ x) (hxL : x ≤ L) (h : Fin d → ℤ) (hh : ∀ (i : Fin d), -L ≤ h i ∧ h i ≤ L) (ω : Fin d → Bool) : -↑d * L ≤ x + cubeShift h ω ∧ x + cubeShift h ω ≤ (↑d + 1) * L

def TrilinearHT.Auto.cyclicCubeIntegerIncrement {L d : ℕ} (x : ZMod (16 * L + 1)) (h : Fin d → ZMod (16 * L + 1)) (i : Fin d) : ℤ

Integer lift of the increment from x to x + h i in the cyclic group.

Equations

• TrilinearHT.Auto.cyclicCubeIntegerIncrement x h i = ↑(x + h i).val - ↑x.val

theorem TrilinearHT.Auto.cyclicCubeIntegerIncrement_cast {L d : ℕ} (x : ZMod (16 * L + 1)) (h : Fin d → ZMod (16 * L + 1)) (i : Fin d) : ↑(cyclicCubeIntegerIncrement x h i) = h i

theorem TrilinearHT.Auto.cyclic_cube_vertex_cast {L d : ℕ} (x : ZMod (16 * L + 1)) (h : Fin d → ZMod (16 * L + 1)) (ω : Fin d → Bool) : ↑(↑x.val + cubeShift (cyclicCubeIntegerIncrement x h) ω) = x + cubeShift h ω

theorem TrilinearHT.Auto.cyclicCubeIntegerIncrement_bounds {L d : ℕ} (x : ZMod (16 * L + 1)) (h : Fin d → ZMod (16 * L + 1)) (hx : x.val < L) (hh : ∀ (i : Fin d), (x + h i).val < L) (i : Fin d) : -↑L ≤ cyclicCubeIntegerIncrement x h i ∧ cyclicCubeIntegerIncrement x h i ≤ ↑L

theorem TrilinearHT.Auto.cyclic_cube_supported_vertex_iff {L : ℕ} (x : ZMod (16 * L + 1)) (h : Fin 3 → ZMod (16 * L + 1)) (hx : x.val < L) (hh : ∀ (i : Fin 3), (x + h i).val < L) (ω : Fin 3 → Bool) : (x + cubeShift h ω).val < L ↔ 0 ≤ ↑x.val + cubeShift (cyclicCubeIntegerIncrement x h) ω ∧ ↑x.val + cubeShift (cyclicCubeIntegerIncrement x h) ω < ↑L

Lattice sampling for cube discretization

The following lattice-sampling section is adapted from ../lean-twocommuting/TwoCommuting/Auto/Sec2ElementaryPreparation.lean, node A04, revision 99879fdcb600af02e0f58867b2ce54100e1deb81. Copyright 2026 Joris Roos; original author Claude; Apache-2.0. It supplies the Banach-valued Riemann-sum step in blueprint lines 1187-1189.

noncomputable def TrilinearHT.Auto.latticeFloor {d : ℕ} (N : ℕ) (x : Fin d → ℝ) : Fin d → ℝ

The lattice point x_h = h ⌊x/h⌋ (coordinatewise) for the mesh h = 1/N (node A04).

Equations

• TrilinearHT.Auto.latticeFloor N x i = ↑⌊↑N * x i⌋ / ↑N

noncomputable def TrilinearHT.Auto.latticeCube {d : ℕ} (N : ℕ) (k : Fin d → ℤ) : Set (Fin d → ℝ)

The half-open lattice cube hk + [0,h)^d with h = 1/N (node A04).

Equations

• TrilinearHT.Auto.latticeCube N k = Set.univ.pi fun (i : Fin d) => Set.Ico (↑(k i) / ↑N) ((↑(k i) + 1) / ↑N)

theorem TrilinearHT.Auto.mem_latticeCube {d N : ℕ} (hN : 0 < N) {k : Fin d → ℤ} {x : Fin d → ℝ} : x ∈ latticeCube N k ↔ ∀ (i : Fin d), ⌊↑N * x i⌋ = k i

theorem TrilinearHT.Auto.volume_latticeCube {d N : ℕ} (hN : 0 < N) (k : Fin d → ℤ) : MeasureTheory.volume (latticeCube N k) = ENNReal.ofReal (↑N)⁻¹ ^ d

theorem TrilinearHT.Auto.abs_sub_latticeFloor_le {d N : ℕ} (hN : 0 < N) (x : Fin d → ℝ) (i : Fin d) : |x i - latticeFloor N x i| ≤ (↑N)⁻¹

theorem TrilinearHT.Auto.tendsto_latticeFloor {d : ℕ} (x : Fin d → ℝ) : Filter.Tendsto (fun (N : ℕ) => latticeFloor N x) Filter.atTop (nhds x)

theorem TrilinearHT.Auto.volume_coord_hyperplane {d : ℕ} (i : Fin d) (a : ℝ) : MeasureTheory.volume {x : Fin d → ℝ | x i = a} = 0

Helper for node A04: coordinate hyperplanes are Lebesgue-null.

theorem TrilinearHT.Auto.lattice_sampling_dominated_convergence {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (H : (Fin d → ℝ) → E) (hHb : ∃ (M : ℝ), ∀ (x : Fin d → ℝ), ‖H x‖ ≤ M) (hHs : ∃ (R : ℝ), ∀ (x : Fin d → ℝ), R < ‖x‖ → H x = 0) (S : Finset (Fin d × ℝ)) (hHc : ∀ (x : Fin d → ℝ), (∀ p ∈ S, x p.1 ≠ p.2) → ContinuousAt H x) : Filter.Tendsto (fun (N : ℕ) => (↑N)⁻¹ ^ d • ∑' (k : Fin d → ℤ), H fun (i : Fin d) => ↑(k i) / ↑N) Filter.atTop (nhds (∫ (x : Fin d → ℝ), H x))

Lemma 2.4 (node A04), lattice sampling. Let H : ℝ^d → E be bounded, vanish outside a bounded set, and be continuous off finitely many coordinate hyperplanes {x_i = a}, (i, a) ∈ S. Then, with mesh h = 1/N, h^d ∑_{k ∈ ℤ^d} H(hk) → ∫ H as N → ∞. Every sum is finite (see lattice_sampling_finite_support).

theorem TrilinearHT.Auto.finiteHaar_pi {I : Type u_1} {G : Type u_2} [Fintype I] [DecidableEq I] [Fintype G] [Nonempty G] [MeasurableSpace G] [MeasurableSingletonClass G] : (MeasureTheory.Measure.pi fun (x : I) => finiteHaar G) = finiteHaar (I → G)

noncomputable def TrilinearHT.Auto.realCubeKernel (g : ℝ → ℂ) (z : Fin 4 → ℝ) : ℂ

Diagonal cube integrand expressed in four independent real coordinates.

Equations

• TrilinearHT.Auto.realCubeKernel g z = TrilinearHT.Auto.diagonalCubeIntegrand 3 g (fun (i : Fin 3) => z i.succ) (z 0)

theorem TrilinearHT.Auto.continuous_realCubeKernel {g : ℝ → ℂ} (hg : Continuous g) : Continuous (realCubeKernel g)

theorem TrilinearHT.Auto.realCubeKernel_norm_le_one (g : ℝ → ℂ) (hg : ∀ (x : ℝ), ‖g x‖ ≤ 1) (z : Fin 4 → ℝ) : ‖realCubeKernel g z‖ ≤ 1

theorem TrilinearHT.Auto.realCubeKernel_eq_zero_outside (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (z : Fin 4 → ℝ) (hz : 1 < ‖z‖) : realCubeKernel g z = 0

theorem TrilinearHT.Auto.realCubeKernel_lattice_limit (g : ℝ → ℂ) (hg : Continuous g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (N : ℕ) => (↑N)⁻¹ ^ 4 • ∑' (k : Fin 4 → ℤ), realCubeKernel g fun (i : Fin 4) => ↑(k i) / ↑N) Filter.atTop (nhds (∫ (z : Fin 4 → ℝ), realCubeKernel g z))

theorem TrilinearHT.Auto.integral_finiteHaar_expect {G : Type u_1} [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (f : G → ℂ) : ∫ (x : G), f x ∂finiteHaar G = Finset.univ.expect fun (x : G) => f x

theorem TrilinearHT.Auto.cubeAverage_finiteHaar_eq_expect {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (j : ℕ) (f : (Fin j → Bool) → G → ℂ) : cubeAverage (finiteHaar G) j f = Finset.univ.expect fun (h : Fin j → G) => Finset.univ.expect fun (x : G) => cubeIntegrand f h x

def TrilinearHT.Auto.cyclicCubeIntegerLift {L : ℕ} (p : ZMod (16 * L + 1) × (Fin 3 → ZMod (16 * L + 1))) : Fin 4 → ℤ

Lift a cyclic base point and three increments to four integer coordinates.

Equations

• TrilinearHT.Auto.cyclicCubeIntegerLift p = Fin.cons (↑p.1.val) (TrilinearHT.Auto.cyclicCubeIntegerIncrement p.1 p.2)

theorem TrilinearHT.Auto.cyclicCubeIntegerLift_injective {L : ℕ} : Function.Injective cyclicCubeIntegerLift

theorem TrilinearHT.Auto.cyclicCubeIntegerLift_of_supported {L : ℕ} (k : Fin 4 → ℤ) (hbase : 0 ≤ k 0 ∧ k 0 < ↑L) (hunit : ∀ (i : Fin 3), 0 ≤ k 0 + k i.succ ∧ k 0 + k i.succ < ↑L) : cyclicCubeIntegerLift (↑(k 0), fun (i : Fin 3) => ↑(k i.succ)) = k

theorem TrilinearHT.Auto.realCubeKernel_lattice_support {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (k : Fin 4 → ℤ) (hk : (realCubeKernel g fun (i : Fin 4) => ↑(k i) / ↑L) ≠ 0) : k ∈ Set.range cyclicCubeIntegerLift

theorem TrilinearHT.Auto.realCubeKernel_lattice_sum {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : (∑' (k : Fin 4 → ℤ), realCubeKernel g fun (i : Fin 4) => ↑(k i) / ↑L) = ∑ p : ZMod (16 * L + 1) × (Fin 3 → ZMod (16 * L + 1)), realCubeKernel g fun (i : Fin 4) => ↑(cyclicCubeIntegerLift p i) / ↑L

theorem TrilinearHT.Auto.supported_sample_vertex {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (x : ZMod (16 * L + 1)) (h : Fin 3 → ZMod (16 * L + 1)) (hx : x.val < L) (hh : ∀ (i : Fin 3), (x + h i).val < L) (ω : Fin 3 → Bool) : g (↑(↑x.val + cubeShift (cyclicCubeIntegerIncrement x h) ω) / ↑L) = g (↑(x + cubeShift h ω).val / ↑L)

theorem TrilinearHT.Auto.realCubeKernel_lift_formula {L : ℕ} (g : ℝ → ℂ) (p : ZMod (16 * L + 1) × (Fin 3 → ZMod (16 * L + 1))) : (realCubeKernel g fun (i : Fin 4) => ↑(cyclicCubeIntegerLift p i) / ↑L) = diagonalCubeIntegrand 3 (fun (a : ℤ) => g (↑a / ↑L)) (cyclicCubeIntegerIncrement p.1 p.2) ↑p.1.val

theorem TrilinearHT.Auto.realCubeKernel_lift_eq_cyclic {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (p : ZMod (16 * L + 1) × (Fin 3 → ZMod (16 * L + 1))) : (realCubeKernel g fun (i : Fin 4) => ↑(cyclicCubeIntegerLift p i) / ↑L) = diagonalCubeIntegrand 3 (fun (j : ZMod (16 * L + 1)) => g (↑j.val / ↑L)) p.2 p.1

theorem TrilinearHT.Auto.cyclic_point_cube_lattice_identity {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : (cubeAverage (finiteHaar (ZMod (16 * L + 1))) 3 fun (x : Fin 3 → Bool) (j : ZMod (16 * L + 1)) => g (↑j.val / ↑L)) = (↑(16 * L + 1))⁻¹ ^ 4 * ∑' (k : Fin 4 → ℤ), realCubeKernel g fun (i : Fin 4) => ↑(k i) / ↑L

theorem TrilinearHT.Auto.cyclic_point_cube_limit (g : ℝ → ℂ) (hg : Continuous g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (L : ℕ) => cubeAverage (finiteHaar (ZMod (16 * L + 1))) 3 fun (x : Fin 3 → Bool) (j : ZMod (16 * L + 1)) => g (↑j.val / ↑L)) Filter.atTop (nhds (16⁻¹ ^ 4 • ∫ (z : Fin 4 → ℝ), realCubeKernel g z))

theorem TrilinearHT.Auto.norm_prod_sub_prod_le_sum {ι : Type u_1} (s : Finset ι) (a b : ι → ℂ) (ha : ∀ i ∈ s, ‖a i‖ ≤ 1) (hb : ∀ i ∈ s, ‖b i‖ ≤ 1) : ‖∏ i ∈ s, a i - ∏ i ∈ s, b i‖ ≤ ∑ i ∈ s, ‖a i - b i‖

theorem TrilinearHT.Auto.norm_cubeIntegrand_sub_le {G : Type u_1} [AddCommMonoid G] (j : ℕ) (f g : (Fin j → Bool) → G → ℂ) (hf : ∀ (ω : Fin j → Bool) (x : G), ‖f ω x‖ ≤ 1) (hg : ∀ (ω : Fin j → Bool) (x : G), ‖g ω x‖ ≤ 1) (h : Fin j → G) (x : G) : ‖cubeIntegrand f h x - cubeIntegrand g h x‖ ≤ ∑ ω : Fin j → Bool, ‖f ω (x + cubeShift h ω) - g ω (x + cubeShift h ω)‖

theorem TrilinearHT.Auto.finite_cubeAverage_uniform_error {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (j : ℕ) (f g : G → ℂ) (hf : ∀ (x : G), ‖f x‖ ≤ 1) (hg : ∀ (x : G), ‖g x‖ ≤ 1) (ε : ℝ) (he : ∀ (x : G), ‖f x - g x‖ ≤ ε) : ‖(cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) => f) - cubeAverage (finiteHaar G) j fun (x : Fin j → Bool) => g‖ ≤ 2 ^ j * ε

theorem TrilinearHT.Auto.cyclicCellAverage_sub_sample_le {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hg : Continuous g) (j : ZMod (16 * L + 1)) (hj : j.val < L) (ε : ℝ) (hosc : ∀ y ∈ Set.uIcc (↑j.val / ↑L) ((↑j.val + 1) / ↑L), ‖g y - g (↑j.val / ↑L)‖ ≤ ε) : ‖cyclicCellAverage L g j - g (↑j.val / ↑L)‖ ≤ ε

theorem TrilinearHT.Auto.cyclicCellAverage_uniform_sample_error (g : ℝ → ℂ) (hg : Continuous g) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (ε : ℝ) (hε : 0 < ε) : ∀ᶠ (L : ℕ) in Filter.atTop, ∀ (j : ZMod (16 * L + 1)), ‖cyclicCellAverage L g j - g (↑j.val / ↑L)‖ ≤ ε

theorem TrilinearHT.Auto.cyclic_cell_cube_limit (g : ℝ → ℂ) (hg : Continuous g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (L : ℕ) => cubeAverage (finiteHaar (ZMod (16 * L + 1))) 3 fun (x : Fin 3 → Bool) => cyclicCellAverage L g) Filter.atTop (nhds (16⁻¹ ^ 4 • ∫ (z : Fin 4 → ℝ), realCubeKernel g z))

theorem TrilinearHT.Auto.instFactLtRealOfNat_leanPool : Fact (0 < 16)

theorem TrilinearHT.Auto.circle_lift_supported_apply (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (v : ℝ) (hv : -8 < v ∧ v < 9) : AddCircle.liftIoc 16 (-8) g ↑v = g v

theorem TrilinearHT.Auto.circle_cube_kernel_on_box (g : ℝ → ℂ) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) (z : Fin 4 → ℝ) (hz : ∀ (i : Fin 4), z i ∈ Set.Ioc (-8) 8) : diagonalCubeIntegrand 3 (AddCircle.liftIoc 16 (-8) g) (fun (i : Fin 3) => ↑(z i.succ)) ↑(z 0) = realCubeKernel g z

theorem TrilinearHT.Auto.cubeAverage_eq_integral_tuple {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] (j : ℕ) (g : G → ℂ) (hg : Measurable g) (hunit : ∀ (x : G), ‖g x‖ ≤ 1) : (cubeAverage μ j fun (x : Fin j → Bool) => g) = ∫ (z : Fin (j + 1) → G), diagonalCubeIntegrand j g (fun (i : Fin j) => z i.succ) (z 0) ∂MeasureTheory.Measure.pi fun (x : Fin (j + 1)) => μ

theorem TrilinearHT.Auto.circle_pi_volume_eq (T : ℝ) [Fact (0 < T)] (d : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume) = ENNReal.ofReal T ^ d • MeasureTheory.Measure.pi fun (x : Fin d) => AddCircle.haarAddCircle

theorem TrilinearHT.Auto.circle_pi_integral_preimage (T : ℝ) [Fact (0 < T)] (d : ℕ) (a : ℝ) (F : (Fin d → AddCircle T) → ℂ) (hF : Measurable F) : (∫ (z : Fin d → AddCircle T), F z ∂MeasureTheory.Measure.pi fun (x : Fin d) => MeasureTheory.volume) = ∫ (z : Fin d → ℝ) in Set.univ.pi fun (x : Fin d) => Set.Ioc a (a + T), F fun (i : Fin d) => ↑(z i)

theorem TrilinearHT.Auto.circle_cube_integral_eq_real (g : ℝ → ℂ) (hg : Measurable g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : (cubeAverage AddCircle.haarAddCircle 3 fun (x : Fin 3 → Bool) => AddCircle.liftIoc 16 (-8) g) = 16⁻¹ ^ 4 • ∫ (z : Fin 4 → ℝ), realCubeKernel g z

theorem TrilinearHT.Auto.cyclic_cell_cube_limit_haar (g : ℝ → ℂ) (hg : Continuous g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (L : ℕ) => cubeAverage (finiteHaar (ZMod (16 * L + 1))) 3 fun (x : Fin 3 → Bool) => cyclicCellAverage L g) Filter.atTop (nhds (cubeAverage AddCircle.haarAddCircle 3 fun (x : Fin 3 → Bool) => AddCircle.liftIoc 16 (-8) g))

Blueprint lem:inverse, lines 1187–1189: the cell-averaged cyclic cube converges to the probability Haar cube of the zero extension to the circle of length 16, for continuous unit-bounded functions supported in the open unit interval.

theorem TrilinearHT.Auto.cubeAverage_L1_error {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (j : ℕ) (f g : G → ℂ) (hf : Measurable f) (hg : Measurable g) (hfu : ∀ (x : G), ‖f x‖ ≤ 1) (hgu : ∀ (x : G), ‖g x‖ ≤ 1) : ‖(cubeAverage μ j fun (x : Fin j → Bool) => f) - cubeAverage μ j fun (x : Fin j → Bool) => g‖ ≤ 2 ^ j * ∫ (x : G), ‖f x - g x‖ ∂μ

Telescoping the bounded cube factors gives the order-j L1 stability bound.

theorem TrilinearHT.Auto.sum_cyclic_initial_segment {E : Type u_1} [AddCommMonoid E] (L : ℕ) (F : ℕ → E) : (∑ j : ZMod (16 * L + 1), if j.val < L then F j.val else 0) = ∑ k ∈ Finset.range L, F k

theorem TrilinearHT.Auto.unit_cell_subset {L k : ℕ} (hL : 0 < L) (hk : k < L) : Set.uIcc (↑k / ↑L) ((↑k + 1) / ↑L) ⊆ Set.uIcc 0 1

theorem TrilinearHT.Auto.cyclicCellAverage_L1_contraction {L : ℕ} (hL : 0 < L) (f g : ℝ → ℂ) (hf : IntervalIntegrable f MeasureTheory.volume 0 1) (hg : IntervalIntegrable g MeasureTheory.volume 0 1) : (Finset.univ.expect fun (j : ZMod (16 * L + 1)) => ‖cyclicCellAverage L f j - cyclicCellAverage L g j‖) ≤ ↑L / (16 * ↑L + 1) * ∫ (x : ℝ) in 0..1, ‖f x - g x‖

theorem TrilinearHT.Auto.integral_finiteHaar_real_expect {G : Type u_1} [Fintype G] [MeasurableSpace G] [MeasurableSingletonClass G] (f : G → ℝ) : ∫ (x : G), f x ∂finiteHaar G = Finset.univ.expect fun (x : G) => f x

noncomputable def TrilinearHT.Auto.unitDiskProjection (z : ℂ) : ℂ

Radial projection of a complex number onto the closed unit disk.

Equations

• TrilinearHT.Auto.unitDiskProjection z = (max 1 ‖z‖)⁻¹ • z

theorem TrilinearHT.Auto.continuous_unitDiskProjection : Continuous unitDiskProjection

theorem TrilinearHT.Auto.unitDiskProjection_zero : unitDiskProjection 0 = 0

theorem TrilinearHT.Auto.unitDiskProjection_norm_le (z : ℂ) : ‖unitDiskProjection z‖ ≤ 1

theorem TrilinearHT.Auto.unitDiskProjection_eq {z : ℂ} (hz : ‖z‖ ≤ 1) : unitDiskProjection z = z

theorem TrilinearHT.Auto.unitDiskProjection_dist_le (z w : ℂ) (hw : ‖w‖ ≤ 1) : ‖unitDiskProjection z - w‖ ≤ ‖z - w‖

theorem TrilinearHT.Auto.bounded_continuous_interior_L1_approximation (g : ℝ → ℂ) (hg : Measurable g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (ε : ℝ) (hε : 0 < ε) : ∃ (h : ℝ → ℂ), Continuous h ∧ HasCompactSupport h ∧ tsupport h ⊆ Set.Ioo 0 1 ∧ (∀ (x : ℝ), ‖h x‖ ≤ 1) ∧ ∫ (x : ℝ) in 0..1, ‖g x - h x‖ ≤ ε

theorem TrilinearHT.Auto.circle_lift_L1_eq (f g : ℝ → ℂ) (hf : ∀ (x : ℝ), f x ≠ 0 → x ∈ Set.Icc 0 1) (hg : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Icc 0 1) : ∫ (z : AddCircle 16), ‖AddCircle.liftIoc 16 (-8) f z - AddCircle.liftIoc 16 (-8) g z‖ ∂AddCircle.haarAddCircle = 16⁻¹ * ∫ (x : ℝ) in 0..1, ‖f x - g x‖

theorem TrilinearHT.Auto.bounded_measurable_intervalIntegrable (g : ℝ → ℂ) (hg : Measurable g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) : IntervalIntegrable g MeasureTheory.volume 0 1

theorem TrilinearHT.Auto.cyclic_cell_cube_limit_haar_bounded (g : ℝ → ℂ) (hg : Measurable g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Icc 0 1) : Filter.Tendsto (fun (L : ℕ) => cubeAverage (finiteHaar (ZMod (16 * L + 1))) 3 fun (x : Fin 3 → Bool) => cyclicCellAverage L g) Filter.atTop (nhds (cubeAverage AddCircle.haarAddCircle 3 fun (x : Fin 3 → Bool) => AddCircle.liftIoc 16 (-8) g))

Blueprint lem:inverse, line 1189: cell-averaged cyclic cube averages converge to the probability Haar cube for every measurable unit-bounded input supported on [0,1].