Section 10: Detection from a local form

This file was automatically generated by Claude.

Formalization of blueprint Section 10, "Detection from a local form" (sec:detection, lines 1418-1479) of blueprint/formalization_blueprint.tex.

noncomputable def TrilinearHT.Auto.unitIntervalL2CircleContinuous : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

Continuous L² embedding from the unit interval into the circle of length sixteen.

Equations

• TrilinearHT.Auto.unitIntervalL2CircleContinuous = TrilinearHT.Auto.unitIntervalL2CircleLinear.mkContinuous 1 ⋯

theorem TrilinearHT.Auto.unitIntervalGowersSeminorm_continuous : Continuous ⇑unitIntervalGowersSeminorm

The generalized von Neumann inequality on a compact abelian group

Blueprint lem:von-neumann, lines 1431–1446: three Cauchy–Schwarz steps bound the progression average by the eighth root of a dilated cube average of the second slot. All inputs here are bounded; the passage to L² is made later.

noncomputable def TrilinearHT.Auto.mulDiff {G : Type u_1} [Add G] (f : G → ℂ) (s y : G) : ℂ

The multiplicative difference f(y) conj f(y + s).

Equations

• TrilinearHT.Auto.mulDiff f s y = f y * (starRingEnd ℂ) (f (y + s))

theorem TrilinearHT.Auto.integral_add_right_haar {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (f : G → ℂ) (a : G) : ∫ (x : G), f (x + a) ∂μ = ∫ (x : G), f x ∂μ

theorem TrilinearHT.Auto.integral_swap_bdd {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {F : X → Y → ℂ} (hF : Measurable (Function.uncurry F)) {M : ℝ} (hM : ∀ (x : X) (y : Y), ‖F x y‖ ≤ M) : ∫ (x : X), ∫ (y : Y), F x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), F x y ∂μ ∂ν

theorem TrilinearHT.Auto.norm_mulDiff_le {G : Type u_1} [Add G] {f : G → ℂ} {M : ℝ} (hf : ∀ (x : G), ‖f x‖ ≤ M) (s y : G) : ‖mulDiff f s y‖ ≤ M * M

theorem TrilinearHT.Auto.measurable_mulDiff {G : Type u_1} [Add G] [MeasurableSpace G] [MeasurableAdd₂ G] {f : G → ℂ} (hf : Measurable f) : Measurable fun (p : G × G) => mulDiff f p.1 p.2

theorem TrilinearHT.Auto.measurable_mulDiff_comp {G : Type u_1} {X : Type u_2} [Add G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableSpace X] {f : G → ℂ} (hf : Measurable f) {s y : X → G} (hs : Measurable s) (hy : Measurable y) : Measurable fun (x : X) => mulDiff f (s x) (y x)

theorem TrilinearHT.Auto.measurable_integral_snd {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν] {F : X → Y → ℂ} (hF : Measurable (Function.uncurry F)) : Measurable fun (x : X) => ∫ (y : Y), F x y ∂ν

theorem TrilinearHT.Auto.norm_integral_le_bound {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {f : X → ℂ} {M : ℝ} (hf : ∀ (x : X), ‖f x‖ ≤ M) : ‖∫ (x : X), f x ∂μ‖ ≤ M

theorem TrilinearHT.Auto.vonNeumann_first_step {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {R g b c : G → ℂ} (hRm : Measurable R) (hgm : Measurable g) (hbm : Measurable b) (hcm : Measurable c) {MR Mg : ℝ} (hR : ∀ (x : G), ‖R x‖ ≤ MR) (hg : ∀ (x : G), ‖g x‖ ≤ Mg) (hb : ∀ (x : G), ‖b x‖ ≤ 1) (hc : ∀ (x : G), ‖c x‖ ≤ 1) (nR ng nb nc : ℤ) : ‖∫ (t : G), ∫ (x : G), R (x + nR • t) * g (x + ng • t) * b (x + nb • t) * c (x + nc • t) ∂μ ∂μ‖ ^ 2 ≤ (∫ (x : G), ‖R x‖ ^ 2 ∂μ) * ∫ (u : G), ‖∫ (t : G), g (u + (ng - nR) • t) * b (u + (nb - nR) • t) * c (u + (nc - nR) • t) ∂μ‖ ^ 2 ∂μ

First Cauchy–Schwarz step (lem:von-neumann, line 1431).

theorem TrilinearHT.Auto.integral_norm_sq_eq_correlation {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {X : Type u_2} [MeasurableSpace X] (ν : MeasureTheory.Measure X) {A : X → G → ℂ} (hA : Measurable (Function.uncurry A)) {M : ℝ} (hM : ∀ (u : X) (t : G), ‖A u t‖ ≤ M) : ↑(∫ (u : X), ‖∫ (t : G), A u t ∂μ‖ ^ 2 ∂ν) = ∫ (u : X), ∫ (h : G), ∫ (t : G), A u t * (starRingEnd ℂ) (A u (t + h)) ∂μ ∂μ ∂ν

The square of an inner average as a correlation (lem:von-neumann, line 1433).

theorem TrilinearHT.Auto.measurable_comp_zsmul_add {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] {X : Type u_2} [MeasurableSpace X] {f : G → ℂ} (hf : Measurable f) {u t : X → G} (hu : Measurable u) (ht : Measurable t) (n : ℤ) : Measurable fun (x : X) => f (u x + n • t x)

theorem TrilinearHT.Auto.integral_three_shift_swap {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {U B V : G → ℂ} (hU : Measurable U) (hB : Measurable B) (hV : Measurable V) {MU MB MV : ℝ} (hUb : ∀ (x : G), ‖U x‖ ≤ MU) (hBb : ∀ (x : G), ‖B x‖ ≤ MB) (hVb : ∀ (x : G), ‖V x‖ ≤ MV) (α β γ : ℤ) : ∫ (u : G), ∫ (t : G), U (u + α • t) * B (u + β • t) * V (u + γ • t) ∂μ ∂μ = ∫ (y : G), B y * ∫ (t : G), U (y + (α - β) • t) * V (y + (γ - β) • t) ∂μ ∂μ

Shift and swap: ∫∫ U(u+αt) B(u+βt) V(u+γt) = ∫ B(y) ∫ U(y+(α-β)t) V(y+(γ-β)t).

theorem TrilinearHT.Auto.norm_integral_two_mul_sq_le {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (ν : MeasureTheory.Measure X) (μ : MeasureTheory.Measure Y) [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure μ] {B K : X → Y → ℂ} (hB : Measurable (Function.uncurry B)) (hK : Measurable (Function.uncurry K)) (hBb : ∀ (h : X) (y : Y), ‖B h y‖ ≤ 1) {M : ℝ} (hKb : ∀ (h : X) (y : Y), ‖K h y‖ ≤ M) : ‖∫ (h : X), ∫ (y : Y), B h y * K h y ∂μ ∂ν‖ ^ 2 ≤ ∫ (h : X), ∫ (y : Y), ‖K h y‖ ^ 2 ∂μ ∂ν

Cauchy–Schwarz on a product of two probability spaces with a 1-bounded first factor.

theorem TrilinearHT.Auto.vonNeumann_second_step {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {g b c : G → ℂ} (hgm : Measurable g) (hbm : Measurable b) (hcm : Measurable c) {Mg : ℝ} (hg : ∀ (x : G), ‖g x‖ ≤ Mg) (hb : ∀ (x : G), ‖b x‖ ≤ 1) (hc : ∀ (x : G), ‖c x‖ ≤ 1) (α β γ : ℤ) : (∫ (u : G), ‖∫ (t : G), g (u + α • t) * b (u + β • t) * c (u + γ • t) ∂μ‖ ^ 2 ∂μ) ^ 2 ≤ ∫ (h : G), ∫ (y : G), ‖∫ (t : G), mulDiff g (α • h) (y + (α - β) • t) * mulDiff c (γ • h) (y + (γ - β) • t) ∂μ‖ ^ 2 ∂μ ∂μ

Second Cauchy–Schwarz step (lem:von-neumann, lines 1433–1436).

theorem TrilinearHT.Auto.integral_two_shift_swap {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {U V : G → ℂ} (hU : Measurable U) (hV : Measurable V) {MU MV : ℝ} (hUb : ∀ (x : G), ‖U x‖ ≤ MU) (hVb : ∀ (x : G), ‖V x‖ ≤ MV) (a c : ℤ) : ∫ (u : G), ∫ (t : G), U (u + a • t) * V (u + c • t) ∂μ ∂μ = ∫ (z : G), V z * ∫ (t : G), U (z + (a - c) • t) ∂μ ∂μ

Shift and swap with two factors: ∫∫ U(u+at) V(u+ct) = ∫ V(z) ∫ U(z+(a-c)t).

theorem TrilinearHT.Auto.integral_norm_sq_shift_avg {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {W : G → ℂ} (hW : Measurable W) {M : ℝ} (hWb : ∀ (x : G), ‖W x‖ ≤ M) (e : ℤ) : ↑(∫ (z : G), ‖∫ (t : G), W (z + e • t) ∂μ‖ ^ 2 ∂μ) = ∫ (h : G), ∫ (z : G), mulDiff W (e • h) z ∂μ ∂μ

The square of an inner progression average, integrated: the last differencing step.

theorem TrilinearHT.Auto.integral_prod_bdd {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (ν : MeasureTheory.Measure X) (μ : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure μ] {F : X × Y → ℂ} (hF : Measurable F) {M : ℝ} (hM : ∀ (p : X × Y), ‖F p‖ ≤ M) : ∫ (p : X × Y), F p ∂ν.prod μ = ∫ (x : X), ∫ (y : Y), F (x, y) ∂μ ∂ν

theorem TrilinearHT.Auto.integral_prod_bdd_real {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (ν : MeasureTheory.Measure X) (μ : MeasureTheory.Measure Y) [MeasureTheory.IsFiniteMeasure ν] [MeasureTheory.IsFiniteMeasure μ] {F : X × Y → ℝ} (hF : Measurable F) {M : ℝ} (hM : ∀ (p : X × Y), ‖F p‖ ≤ M) : ∫ (p : X × Y), F p ∂ν.prod μ = ∫ (x : X), ∫ (y : Y), F (x, y) ∂μ ∂ν

theorem TrilinearHT.Auto.vonNeumann_third_step {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {U V : G → G → ℂ} (hUm : Measurable (Function.uncurry U)) (hVm : Measurable (Function.uncurry V)) {MU : ℝ} (hU : ∀ (p x : G), ‖U p x‖ ≤ MU) (hV : ∀ (p x : G), ‖V p x‖ ≤ 1) (a c : ℤ) : (∫ (p : G), ∫ (y : G), ‖∫ (t : G), U p (y + a • t) * V p (y + c • t) ∂μ‖ ^ 2 ∂μ ∂μ) ^ 2 ≤ ∫ (p : G), ∫ (h : G), ∫ (z : G), ‖∫ (t : G), mulDiff (U p) (a • h) (z + (a - c) • t) ∂μ‖ ^ 2 ∂μ ∂μ ∂μ

Third Cauchy–Schwarz step (lem:von-neumann, lines 1436–1440), with an outer parameter.

noncomputable def TrilinearHT.Auto.dilatedCube {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (g : G → ℂ) (a b c : ℤ) : ℂ

The dilated third multiplicative difference average of g.

Equations

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

theorem TrilinearHT.Auto.vonNeumann_group_bounded {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] {R g b c : G → ℂ} (hRm : Measurable R) (hgm : Measurable g) (hbm : Measurable b) (hcm : Measurable c) {MR Mg : ℝ} (hR : ∀ (x : G), ‖R x‖ ≤ MR) (hg : ∀ (x : G), ‖g x‖ ≤ Mg) (hb : ∀ (x : G), ‖b x‖ ≤ 1) (hc : ∀ (x : G), ‖c x‖ ≤ 1) (nR ng nb nc : ℤ) : ‖∫ (t : G), ∫ (x : G), R (x + nR • t) * g (x + ng • t) * b (x + nb • t) * c (x + nc • t) ∂μ ∂μ‖ ^ 8 ≤ (∫ (x : G), ‖R x‖ ^ 2 ∂μ) ^ 4 * (dilatedCube μ g (ng - nR) (ng - nb) (ng - nc)).re

Blueprint lem:von-neumann, lines 1431–1446, for bounded inputs on a compact abelian group with Haar probability: |Λ|⁸ ≤ ‖R‖₂⁸ · (dilated U³ average of g) when |b|,|c| ≤ 1.

Identification with the Gowers U³ norm (lem:von-neumann, line 1447)

theorem TrilinearHT.Auto.measurable_mulDiff₂ {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] {g : G → ℂ} (hg : Measurable g) : Measurable fun (p : (G × G) × G) => mulDiff (mulDiff g p.1.1) p.1.2 p.2

theorem TrilinearHT.Auto.measurable_mulDiff₃ {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] {g : G → ℂ} (hg : Measurable g) : Measurable fun (p : ((G × G) × G) × G) => mulDiff (mulDiff (mulDiff g p.1.1.1) p.1.1.2) p.1.2 p.2

theorem TrilinearHT.Auto.measurable_fin_cons_pair {G : Type u_1} [MeasurableSpace G] {n : ℕ} : Measurable fun (p : (Fin n → G) × G) => Fin.cons p.2 p.1

theorem TrilinearHT.Auto.diagonalCubeIntegrand_three {G : Type u_1} [AddCommGroup G] (g : G → ℂ) (r s t x : G) : diagonalCubeIntegrand 3 g (Fin.cons t (Fin.cons s (Fin.cons r Fin.elim0))) x = mulDiff (mulDiff (mulDiff g r) s) t x

theorem TrilinearHT.Auto.cubeAverage_three_eq_nested {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {g : G → ℂ} (hg : Measurable g) {M : ℝ} (hgb : ∀ (x : G), ‖g x‖ ≤ M) : (cubeAverage μ 3 fun (x : Fin 3 → Bool) => g) = ∫ (r : G), ∫ (s : G), ∫ (t : G), ∫ (z : G), mulDiff (mulDiff (mulDiff g r) s) t z ∂μ ∂μ ∂μ ∂μ

The order-three cube average as an iterated integral of multiplicative differences.

theorem TrilinearHT.Auto.integral_comp_measurePreserving_self {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) {φ : G → G} (hmp : MeasureTheory.MeasurePreserving φ μ μ) {F : G → ℂ} (hF : Measurable F) : ∫ (h : G), F (φ h) ∂μ = ∫ (h : G), F h ∂μ

theorem TrilinearHT.Auto.measurable_cube_partial₁ {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {g : G → ℂ} (hg : Measurable g) (β γ : ℤ) : Measurable fun (k : G) => ∫ (s : G), ∫ (t : G), ∫ (z : G), mulDiff (mulDiff (mulDiff g k) (β • s)) (γ • t) z ∂μ ∂μ ∂μ

theorem TrilinearHT.Auto.measurable_cube_partial₂ {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {g : G → ℂ} (hg : Measurable g) (r : G) (γ : ℤ) : Measurable fun (s : G) => ∫ (t : G), ∫ (z : G), mulDiff (mulDiff (mulDiff g r) s) (γ • t) z ∂μ ∂μ

theorem TrilinearHT.Auto.measurable_cube_partial₃ {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] {g : G → ℂ} (hg : Measurable g) (r s : G) : Measurable fun (t : G) => ∫ (z : G), mulDiff (mulDiff (mulDiff g r) s) t z ∂μ

theorem TrilinearHT.Auto.dilatedCube_eq_nested {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] (hdil : ∀ (n : ℤ), n ≠ 0 → MeasureTheory.MeasurePreserving (fun (h : G) => n • h) μ μ) {g : G → ℂ} (hg : Measurable g) {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) : dilatedCube μ g a b c = ∫ (r : G), ∫ (s : G), ∫ (t : G), ∫ (z : G), mulDiff (mulDiff (mulDiff g r) s) t z ∂μ ∂μ ∂μ ∂μ

Integer dilations of the increments do not change the cube average when every nonzero integer multiplication preserves the Haar probability (lem:von-neumann, line 1447).

theorem TrilinearHT.Auto.vonNeumann_group_U3 {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] (hdil : ∀ (n : ℤ), n ≠ 0 → MeasureTheory.MeasurePreserving (fun (h : G) => n • h) μ μ) {R g b c : G → ℂ} (hRm : Measurable R) (hgm : Measurable g) (hbm : Measurable b) (hcm : Measurable c) {MR Mg : ℝ} (hR : ∀ (x : G), ‖R x‖ ≤ MR) (hg : ∀ (x : G), ‖g x‖ ≤ Mg) (hb : ∀ (x : G), ‖b x‖ ≤ 1) (hc : ∀ (x : G), ‖c x‖ ≤ 1) {nR ng nb nc : ℤ} (h1 : ng ≠ nR) (h2 : ng ≠ nb) (h3 : ng ≠ nc) : ‖∫ (t : G), ∫ (x : G), R (x + nR • t) * g (x + ng • t) * b (x + nb • t) * c (x + nc • t) ∂μ ∂μ‖ ^ 8 ≤ (∫ (x : G), ‖R x‖ ^ 2 ∂μ) ^ 4 * gowersNorm μ 3 g ^ 8

lem:von-neumann, lines 1431–1447, on a compact abelian group whose nonzero integer multiplications preserve the Haar probability: |Λ|⁸ ≤ ‖R‖₂⁸ ‖g‖_{U³}⁸ for |b|,|c| ≤ 1.

theorem TrilinearHT.Auto.addCircle_zsmul_surjective {T : ℝ} {n : ℤ} (hn : n ≠ 0) : Function.Surjective fun (x : AddCircle T) => n • x

theorem TrilinearHT.Auto.addCircle_zsmul_measurePreserving {T : ℝ} [Fact (0 < T)] {n : ℤ} (hn : n ≠ 0) : MeasureTheory.MeasurePreserving (fun (x : AddCircle T) => n • x) AddCircle.haarAddCircle AddCircle.haarAddCircle

noncomputable def TrilinearHT.Auto.torusLift (F : ℝ → ℂ) : AddCircle 16 → ℂ

Lifting a function supported in [0,1) to the torus of length 16.

Equations

• TrilinearHT.Auto.torusLift F = AddCircle.liftIoc 16 (-8) F

theorem TrilinearHT.Auto.torusLift_coe {F : ℝ → ℂ} {u : ℝ} (hu : u ∈ Set.Ioc (-8) 8) : torusLift F ↑u = F u

theorem TrilinearHT.Auto.torusLift_ne_zero_shift {F : ℝ → ℂ} (hsupp : ∀ (y : ℝ), F y ≠ 0 → y ∈ Set.Ico 0 1) {u s : ℝ} (hu : u ∈ Set.Ico 0 1) (hs : s ∈ Set.Ioc (-8) 8) (h : torusLift F ↑(u + s) ≠ 0) : |s| < 1 ∧ torusLift F ↑(u + s) = F (u + s)

No wraparound: a nonzero lifted value at u + s with u ∈ [0,1) forces s ∈ (-1,1).

theorem TrilinearHT.Auto.coe_add_zsmul_circle (u s : ℝ) (n : ℤ) : ↑(u + ↑n * s) = ↑u + n • ↑s

theorem TrilinearHT.Auto.torus_progression_product (F : Fin 4 → ℝ → ℂ) (hsupp : ∀ (j : Fin 4) (y : ℝ), F j y ≠ 0 → y ∈ Set.Ico 0 1) {u s : ℝ} (hu : u ∈ Set.Ioc (-8) 8) (hs : s ∈ Set.Ioc (-8) 8) : ∏ j : Fin 4, torusLift (F j) (↑u + ↑↑j • ↑s) = ∏ j : Fin 4, F j (u + ↑↑j * s)

On the fundamental box the lifted progression product is the real one.

theorem TrilinearHT.Auto.integral_haarAddCircle_sixteen {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (φ : AddCircle 16 → E) : ∫ (t : AddCircle 16), φ t ∂AddCircle.haarAddCircle = 16⁻¹ • ∫ (a : ℝ) in Set.Ioc (-8) 8, φ ↑a

theorem TrilinearHT.Auto.real_progression_eq_torus (F : Fin 4 → ℝ → ℂ) (hsupp : ∀ (j : Fin 4) (y : ℝ), F j y ≠ 0 → y ∈ Set.Ico 0 1) : ∫ (s : ℝ) (u : ℝ), ∏ j : Fin 4, F j (u + ↑↑j * s) = 256 • ∫ (t : AddCircle 16), ∫ (x : AddCircle 16), ∏ j : Fin 4, torusLift (F j) (x + ↑↑j • t) ∂AddCircle.haarAddCircle ∂AddCircle.haarAddCircle

Blueprint lem:von-neumann, line 1429: the real progression integral of functions supported in [0,1) is 16² times the progression average on the torus of length 16.

theorem TrilinearHT.Auto.prod_fin_four_perm {M : Type u_1} [CommMonoid M] (φ : Fin 4 → M) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : ∏ j : Fin 4, φ j = φ a * φ b * φ c * φ d

theorem TrilinearHT.Auto.measurable_torusLift {F : ℝ → ℂ} (hF : Measurable F) : Measurable (torusLift F)

theorem TrilinearHT.Auto.norm_torusLift_le {F : ℝ → ℂ} {M : ℝ} (hF : ∀ (y : ℝ), ‖F y‖ ≤ M) (x : AddCircle 16) : ‖torusLift F x‖ ≤ M

theorem TrilinearHT.Auto.integral_norm_sq_torusLift {F : ℝ → ℂ} (hsupp : ∀ (y : ℝ), F y ≠ 0 → y ∈ Set.Ico 0 1) : ∫ (x : AddCircle 16), ‖torusLift F x‖ ^ 2 ∂AddCircle.haarAddCircle = 16⁻¹ * ∫ (y : ℝ), ‖F y‖ ^ 2

theorem TrilinearHT.Auto.fin_cast_int_ne {a b : Fin 4} (h : a ≠ b) : ↑↑a ≠ ↑↑b

theorem TrilinearHT.Auto.progression_term_bound (F : Fin 4 → ℝ → ℂ) (hF : ∀ (j : Fin 4), Measurable (F j)) (hsupp : ∀ (j : Fin 4) (y : ℝ), F j y ≠ 0 → y ∈ Set.Ico 0 1) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) {MR Mg : ℝ} (hR : ∀ (y : ℝ), ‖F jR y‖ ≤ MR) (hg : ∀ (y : ℝ), ‖F ig y‖ ≤ Mg) (hb : ∀ (y : ℝ), ‖F kb y‖ ≤ 1) (hc : ∀ (y : ℝ), ‖F lc y‖ ≤ 1) : ‖∫ (s : ℝ) (u : ℝ), ∏ j : Fin 4, F j (u + ↑↑j * s)‖ ≤ 64 * √(∫ (y : ℝ), ‖F jR y‖ ^ 2) * gowersNorm AddCircle.haarAddCircle 3 (torusLift (F ig))

One progression term on the unit cell: Plancherel-free von Neumann bound through the torus.

theorem TrilinearHT.Auto.progression_integral_rescale {r : ℝ} (hr : 0 < r) (a₀ : ℝ) (Φ : ℝ × ℝ → ℂ) (hΦ : MeasureTheory.Integrable Φ MeasureTheory.volume) : ∫ (z : ℝ × ℝ), Φ z = r ^ 2 • ∫ (s : ℝ) (u : ℝ), Φ (a₀ + r * u, r * s)

Affine rescaling of a progression integral over ℝ² to the unit scale.

theorem TrilinearHT.Auto.linear_phase_two_slots (α β x t : ℝ) {p q : ℝ} (hpq : p ≠ q) : α * x + β * t = (α - (β - p * α) / (q - p)) * (x + p * t) + (β - p * α) / (q - p) * (x + q * t)

A linear phase in (x,t) is a product of linear phases in two distinct slots.

noncomputable def TrilinearHT.Auto.charSlotInput (a₀ r : ℝ) (f : Fin 4 → ℝ → ℂ) (jR kb : Fin 4) (αR αb : ℝ) (j : Fin 4) (u : ℝ) : ℂ

The slot-modulated, rescaled inputs of one kernel character term.

Equations

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

theorem TrilinearHT.Auto.integrable_progression_four {G : Fin 4 → ℝ → ℂ} (hG : ∀ (j : Fin 4), Measurable (G j)) {M : ℝ} (hGb : ∀ (j : Fin 4) (y : ℝ), ‖G j y‖ ≤ M) {a b : ℝ} (hsupp : ∀ (j : Fin 4) (y : ℝ), G j y ≠ 0 → y ∈ Set.Ico a b) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => ∏ j : Fin 4, G j (z.1 + ↑↑j * z.2)) MeasureTheory.volume

theorem TrilinearHT.Auto.fin_four_cover {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (j : Fin 4) : j = a ∨ j = b ∨ j = c ∨ j = d

theorem TrilinearHT.Auto.charSlotInput_norm_le {a₀ r : ℝ} (hr : 0 < r) (f : Fin 4 → ℝ → ℂ) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h6 : kb ≠ lc) {MR Mg : ℝ} (hMR : 0 ≤ MR) (hMg : 0 ≤ Mg) (hR : ∀ (y : ℝ), ‖f jR y‖ ≤ MR) (hg : ∀ (y : ℝ), ‖f ig y‖ ≤ Mg) (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ 1) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ 1) (αR αb u : ℝ) : ‖charSlotInput a₀ r f jR kb αR αb jR u‖ ≤ MR ∧ ‖charSlotInput a₀ r f jR kb αR αb ig u‖ ≤ Mg ∧ ‖charSlotInput a₀ r f jR kb αR αb kb u‖ ≤ 1 ∧ ‖charSlotInput a₀ r f jR kb αR αb lc u‖ ≤ 1

theorem TrilinearHT.Auto.indicator_affine_unit {a₀ r : ℝ} (hr : 0 < r) (φ : ℝ → ℂ) (v : ℝ) : (Set.Ico a₀ (a₀ + r)).indicator φ (a₀ + r * v) = (Set.Ico 0 1).indicator (fun (y : ℝ) => φ (a₀ + r * y)) v

theorem TrilinearHT.Auto.char_term_pointwise {a₀ r : ℝ} (hr : 0 < r) (f : Fin 4 → ℝ → ℂ) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) (α β θ u s : ℝ) : ↑(Real.fourierChar (θ + α * (a₀ + r * u) + β * (r * s))) * ∏ j : Fin 4, (Set.Ico a₀ (a₀ + r)).indicator (f j) (a₀ + r * u + ↑↑j * (r * s)) = ↑(Real.fourierChar θ) * ∏ j : Fin 4, charSlotInput a₀ r f jR kb (α - (β - ↑↑jR * α) / (↑↑kb - ↑↑jR)) ((β - ↑↑jR * α) / (↑↑kb - ↑↑jR)) j (u + ↑↑j * s)

theorem TrilinearHT.Auto.integral_indicator_affine_unit {a₀ r : ℝ} (hr : 0 < r) (g : ℝ → ℝ) : ∫ (y : ℝ), (Set.Ico 0 1).indicator (fun (y : ℝ) => g (a₀ + r * y)) y = r⁻¹ * ∫ (x : ℝ) in Set.Ico a₀ (a₀ + r), g x

theorem TrilinearHT.Auto.kernel_character_term_bound {a₀ r : ℝ} (hr : 0 < r) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) {MR Mg : ℝ} (hR : ∀ (y : ℝ), ‖f jR y‖ ≤ MR) (hg : ∀ (y : ℝ), ‖f ig y‖ ≤ Mg) (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ 1) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ 1) (α β θ : ℝ) : ‖∫ (z : ℝ × ℝ), ↑(Real.fourierChar (θ + α * z.1 + β * z.2)) * ∏ j : Fin 4, (Set.Ico a₀ (a₀ + r)).indicator (f j) (z.1 + ↑↑j * z.2)‖ ≤ r ^ 2 * (64 * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖f jR y‖ ^ 2) * intervalGowersNorm a₀ (a₀ + r) (f ig))

lem:von-neumann, lines 1427–1429: one kernel character term.

theorem TrilinearHT.Auto.vonNeumann_local_bounded {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) {MR Mg : ℝ} (hR : ∀ (y : ℝ), ‖f jR y‖ ≤ MR) (hg : ∀ (y : ℝ), ‖f ig y‖ ≤ Mg) (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ 1) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ 1) : ‖localProgressionForm r w f‖ ≤ kernelFourierConst κ * (64 * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖f jR y‖ ^ 2) * intervalGowersNorm a₀ (a₀ + r) (f ig))

Blueprint lem:von-neumann for bounded inputs: for any ordering of four distinct slots, |H_I(R,g,b,c)| ≤ C ‖R‖_{2,I} ‖g‖_{U(I)} when |b|,|c| ≤ 1 on I, with C depending only on the kernel class.

theorem TrilinearHT.Auto.normalizedIntervalMeasure_eq_intervalProbability (a : ℝ) {r : ℝ} (hr : 0 < r) : normalizedIntervalMeasure a r = intervalProbabilityMeasure a (a + r)

theorem TrilinearHT.Auto.localProgression_integrand_restrict {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (z : ℝ × ℝ) : w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z) = w z * ∏ j : Fin 4, (Set.Ico a₀ (a₀ + r)).indicator (f j) (realProgressionCoordinate j z)

Only the restrictions of the inputs to the cell enter an admissible local form.

theorem TrilinearHT.Auto.localProgressionForm_eq_zero_of_vanish {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (k : Fin 4) (hk : ∀ y ∈ Set.Ico a₀ (a₀ + r), f k y = 0) : localProgressionForm r w f = 0

An admissible local form vanishes when one input vanishes on the cell.

theorem TrilinearHT.Auto.localProgressionForm_update_smul (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (k : Fin 4) (c : ℂ) : localProgressionForm r w (Function.update f k (c • f k)) = c * localProgressionForm r w f

Scaling one input scales the local form.

noncomputable def TrilinearHT.Auto.truncateNorm (n : ℝ) (f : ℝ → ℂ) : ℝ → ℂ

Truncation of a function at a norm level.

Equations

• TrilinearHT.Auto.truncateNorm n f = {y : ℝ | ‖f y‖ ≤ n}.indicator f

theorem TrilinearHT.Auto.truncateNorm_measurable {f : ℝ → ℂ} (hf : Measurable f) (n : ℝ) : Measurable (truncateNorm n f)

theorem TrilinearHT.Auto.norm_truncateNorm_le_level {n : ℝ} (hn : 0 ≤ n) (f : ℝ → ℂ) (y : ℝ) : ‖truncateNorm n f y‖ ≤ n

theorem TrilinearHT.Auto.norm_truncateNorm_le (n : ℝ) (f : ℝ → ℂ) (y : ℝ) : ‖truncateNorm n f y‖ ≤ ‖f y‖

theorem TrilinearHT.Auto.tendsto_truncateNorm (f : ℝ → ℂ) (y : ℝ) : Filter.Tendsto (fun (n : ℕ) => truncateNorm (↑n) f y) Filter.atTop (nhds (f y))

theorem TrilinearHT.Auto.tendsto_eLpNorm_truncateNorm {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℂ} (hfm : Measurable f) (hf : MeasureTheory.MemLp f 2 μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f - truncateNorm (↑n) f) 2 μ) Filter.atTop (nhds 0)

theorem TrilinearHT.Auto.integrable_localProgression {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm ((Set.Ico a₀ (a₀ + r)).indicator (f j)) (p j) (normalizedIntervalMeasure a₀ r) ≠ ⊤) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume

Integrability of an admissible local progression integrand whose cell restrictions have finite normalized norms at exponents allowed by eq:absolute.

theorem TrilinearHT.Auto.memLp_normalized_indicator {a₀ r : ℝ} {g : ℝ → ℂ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : MeasureTheory.MemLp ((Set.Ico a₀ (a₀ + r)).indicator g) 2 (normalizedIntervalMeasure a₀ r)

theorem TrilinearHT.Auto.eLpNorm_top_indicator_le {a₀ r : ℝ} {g : ℝ → ℂ} (hgm : Measurable g) {M : ℝ} (hg : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖g y‖ ≤ M) (μ : MeasureTheory.Measure ℝ) : MeasureTheory.eLpNorm ((Set.Ico a₀ (a₀ + r)).indicator g) ⊤ μ ≤ ENNReal.ofReal (max M 0)

theorem TrilinearHT.Auto.vonNeumann_local_L2_unit {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) (hR : MeasureTheory.MemLp (f jR) 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hg : MeasureTheory.MemLp (f ig) 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ 1) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ 1) : ‖localProgressionForm r w f‖ ≤ kernelFourierConst κ * (64 * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖f jR y‖ ^ 2) * intervalGowersNorm a₀ (a₀ + r) (f ig))

Blueprint lem:von-neumann, line 1447: passage from bounded inputs to L² inputs by truncation, for |b|, |c| ≤ 1 on the cell.

theorem TrilinearHT.Auto.intervalGowersNorm_nonneg_of_memLp {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hgm : Measurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) : 0 ≤ intervalGowersNorm a₀ (a₀ + r) g

theorem TrilinearHT.Auto.vonNeumann_local_L2 {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) (hR : MeasureTheory.MemLp (f jR) 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) (hg : MeasureTheory.MemLp (f ig) 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))) {Mb Mc : ℝ} (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ Mb) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ Mc) : ‖localProgressionForm r w f‖ ≤ kernelFourierConst κ * (64 * √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖f jR y‖ ^ 2) * intervalGowersNorm a₀ (a₀ + r) (f ig)) * Mb * Mc

Blueprint lem:von-neumann, eq:von-neumann: for any ordering of four distinct slots, R, g ∈ L²(I) and b, c bounded on I, |H_I(R,g,b,c)| ≤ C ‖R‖_{2,I} ‖g‖_{U(I)} ‖b‖_∞ ‖c‖_∞.

noncomputable def TrilinearHT.Auto.vonNeumannConst (κ : LocalKernelClass) : ℝ

The constant of lem:von-neumann for the fixed admissible kernel class.

Equations

• TrilinearHT.Auto.vonNeumannConst κ = max (TrilinearHT.Auto.kernelFourierConst κ * 64) (2 * TrilinearHT.Auto.localKernelSupBound κ)

theorem TrilinearHT.Auto.vonNeumannConst_nonneg (κ : LocalKernelClass) : 0 ≤ vonNeumannConst κ

theorem TrilinearHT.Auto.vonNeumann_local_L1 {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) : ‖localProgressionForm r w f‖ₑ ≤ ENNReal.ofReal (vonNeumannConst κ) * (MeasureTheory.eLpNorm (f jR) 1 (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f ig) 1 (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f kb) ⊤ (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f lc) ⊤ (normalizedIntervalMeasure a₀ r))

Blueprint lem:von-neumann, the L¹ assertion: the two-coordinate case of lem:absolute with R, g ∈ L¹(I) and b, c ∈ L^∞(I).

theorem TrilinearHT.Auto.sum_fin_four_perm {M : Type u_1} [AddCommMonoid M] (φ : Fin 4 → M) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) : ∑ j : Fin 4, φ j = φ a + φ b + φ c + φ d

theorem TrilinearHT.Auto.eLpNorm_sub_truncateNorm_le {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℂ} (hf : Measurable f) {p q B : ℝ} (hp : 0 < p) (hpq : p ≤ q) (hB : 0 < B) : MeasureTheory.eLpNorm (f - truncateNorm B f) (ENNReal.ofReal p) μ ≤ ENNReal.ofReal (B ^ (1 - q / p)) * MeasureTheory.eLpNorm f (ENNReal.ofReal q) μ ^ (q / p)

Tail estimate for norm truncation: for 0 < p ≤ q, the part of f above level B has L^p norm at most B^(1 - q/p) ‖f‖_q^(q/p).

theorem TrilinearHT.Auto.prod_update_eval (f : Fin 4 → ℝ → ℂ) (k : Fin 4) (g : ℝ → ℂ) (y : Fin 4 → ℝ) : ∏ j : Fin 4, Function.update f k g j (y j) = g (y k) * ∏ j ∈ Finset.univ.erase k, f j (y j)

Evaluating a product after replacing one input.

theorem TrilinearHT.Auto.localProgressionForm_update_add (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (k : Fin 4) (g₁ g₂ : ℝ → ℂ) (h₁ : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, Function.update f k g₁ j (realProgressionCoordinate j z)) MeasureTheory.volume) (h₂ : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, Function.update f k g₂ j (realProgressionCoordinate j z)) MeasureTheory.volume) : localProgressionForm r w (Function.update f k (g₁ + g₂)) = localProgressionForm r w (Function.update f k g₁) + localProgressionForm r w (Function.update f k g₂)

Additivity of the local form in one input.

theorem TrilinearHT.Auto.integrable_localProgression_two {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)) MeasureTheory.volume

Integrability of an admissible local integrand with four normalized L² inputs.

theorem TrilinearHT.Auto.localProgressionForm_enorm_le_slots {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (pa pb pc pd : ENNReal) (ha : 1 ≤ pa) (hb : 1 ≤ pb) (hc : 1 ≤ pc) (hd : 1 ≤ pd) (hsum : pa.toReal⁻¹ + pb.toReal⁻¹ + pc.toReal⁻¹ + pd.toReal⁻¹ ≤ 2) : ‖localProgressionForm r w f‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * (MeasureTheory.eLpNorm (f a) pa (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f b) pb (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f c) pc (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f d) pd (normalizedIntervalMeasure a₀ r))

eq:absolute with exponents assigned to four distinct slots.

noncomputable def TrilinearHT.Auto.clipExcept (B : ℝ) (k : Fin 4) (f : Fin 4 → ℝ → ℂ) : Fin 4 → ℝ → ℂ

Clipping every input except the one in slot k at height B.

Equations

• TrilinearHT.Auto.clipExcept B k f j = if j = k then f j else TrilinearHT.Auto.truncateNorm B (f j)

theorem TrilinearHT.Auto.eLpNorm_update_ne_top {μ : MeasureTheory.Measure ℝ} {p : ENNReal} {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) p μ ≠ ⊤) (k : Fin 4) {g : ℝ → ℂ} (hg : MeasureTheory.eLpNorm g p μ ≠ ⊤) (j : Fin 4) : MeasureTheory.eLpNorm (Function.update f k g j) p μ ≠ ⊤

theorem TrilinearHT.Auto.measurable_update_slot {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (k : Fin 4) {g : ℝ → ℂ} (hg : Measurable g) (j : Fin 4) : Measurable (Function.update f k g j)

theorem TrilinearHT.Auto.norm_le_of_enorm_le_four {x : ℂ} {W α β γ ε : ℝ} (hW : 0 ≤ W) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hγ : 0 ≤ γ) (hε : 0 ≤ ε) {A B C D : ENNReal} (h : ‖x‖ₑ ≤ ENNReal.ofReal W * (A * B * C * D)) (hA : A ≤ ENNReal.ofReal α) (hB : B ≤ ENNReal.ofReal β) (hC : C ≤ ENNReal.ofReal γ) (hD : D ≤ ENNReal.ofReal ε) : ‖x‖ ≤ W * (α * β * γ * ε)

theorem TrilinearHT.Auto.detection_clipping {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ih ku lv : Fin 4} (h1 : jR ≠ ih) (h2 : jR ≠ ku) (h3 : jR ≠ lv) (h4 : ih ≠ ku) (h5 : ih ≠ lv) (h6 : ku ≠ lv) {q C₁ B : ℝ} (hq : 2 < q) (hC₁ : 0 ≤ C₁) (hB1 : 1 ≤ B) (hR : MeasureTheory.eLpNorm (f jR) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁) (hh : MeasureTheory.eLpNorm (f ih) (ENNReal.ofReal q) (normalizedIntervalMeasure a₀ r) ≤ 1) (hu : MeasureTheory.eLpNorm (f ku) 2 (normalizedIntervalMeasure a₀ r) ≤ 1) (hv : MeasureTheory.eLpNorm (f lv) 2 (normalizedIntervalMeasure a₀ r) ≤ 1) : ‖localProgressionForm r w f‖ ≤ ‖localProgressionForm r w (clipExcept B jR f)‖ + 3 * (localFormUniformConstant κ * (C₁ * B ^ (-(q - 2) / q) * 1 * 1))

Blueprint lem:detection, lines 1465-1467: clipping the three opponents of R at height B changes the local form by at most 3 C C₁ B^{-(q-2)/q}.

theorem TrilinearHT.Auto.localProgressionForm_update_const_smul (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) (k : Fin 4) (c : ℂ) (g : ℝ → ℂ) : localProgressionForm r w (Function.update f k (c • g)) = c * localProgressionForm r w (Function.update f k g)

Homogeneity of the local form in one input.

theorem TrilinearHT.Auto.localProgressionForm_update_add_two {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (k : Fin 4) {g₁ g₂ : ℝ → ℂ} (hg₁ : Measurable g₁) (hg₂ : Measurable g₂) (hg₁f : MeasureTheory.eLpNorm g₁ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hg₂f : MeasureTheory.eLpNorm g₂ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : localProgressionForm r w (Function.update f k (g₁ + g₂)) = localProgressionForm r w (Function.update f k g₁) + localProgressionForm r w (Function.update f k g₂)

Additivity in one slot when every input has finite normalized L² norm.

theorem TrilinearHT.Auto.localProgressionForm_update_sum {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (k : Fin 4) {ι : Type u_1} (s : Finset ι) (c : ι → ℂ) (φ : ι → ℝ → ℂ) (hφ : ∀ (i : ι), Measurable (φ i)) (hφf : ∀ (i : ι), MeasureTheory.eLpNorm (φ i) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : localProgressionForm r w (Function.update f k fun (x : ℝ) => ∑ i ∈ s, c i * φ i x) = ∑ i ∈ s, c i * localProgressionForm r w (Function.update f k (φ i))

Linearity in one slot over a finite sum of finite-norm inputs.

theorem TrilinearHT.Auto.localProgressionForm_update_congr_ae {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {f : Fin 4 → ℝ → ℂ} (hf : ∀ (j : Fin 4), Measurable (f j)) (hfin : ∀ (j : Fin 4), MeasureTheory.eLpNorm (f j) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) {g₁ g₂ : ℝ → ℂ} (hg₁ : Measurable g₁) (hg₂ : Measurable g₂) (hg₁f : MeasureTheory.eLpNorm g₁ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hg₂f : MeasureTheory.eLpNorm g₂ 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hae : g₁ =ᵐ[normalizedIntervalMeasure a₀ r] g₂) : localProgressionForm r w (Function.update f a g₁) = localProgressionForm r w (Function.update f a g₂)

The local form only sees an input up to a.e. equality on the cell.

theorem TrilinearHT.Auto.fin4_eq_of_distinct (jR ig kb lc j : Fin 4) : jR ≠ ig → jR ≠ kb → jR ≠ lc → ig ≠ kb → ig ≠ lc → kb ≠ lc → j = jR ∨ j = ig ∨ j = kb ∨ j = lc

Four distinct elements exhaust Fin 4.

theorem TrilinearHT.Auto.memLp_Ico_of_normalized {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hg : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ico a₀ (a₀ + r)))

theorem TrilinearHT.Auto.sqrt_normalized_le_of_eLpNorm {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} {C : ℝ} (hC : 0 ≤ C) (hg : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C) : √(r⁻¹ * ∫ (y : ℝ) in Set.Ico a₀ (a₀ + r), ‖g y‖ ^ 2) ≤ C

theorem TrilinearHT.Auto.vonNeumann_local_L2_const {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {jR ig kb lc : Fin 4} (h1 : jR ≠ ig) (h2 : jR ≠ kb) (h3 : jR ≠ lc) (h4 : ig ≠ kb) (h5 : ig ≠ lc) (h6 : kb ≠ lc) {C₁ Mb Mc : ℝ} (hC₁ : 0 ≤ C₁) (hR : MeasureTheory.eLpNorm (f jR) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁) (hg : MeasureTheory.eLpNorm (f ig) 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) (hb : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f kb y‖ ≤ Mb) (hc : ∀ y ∈ Set.Ico a₀ (a₀ + r), ‖f lc y‖ ≤ Mc) : ‖localProgressionForm r w f‖ ≤ vonNeumannConst κ * C₁ * intervalGowersNorm a₀ (a₀ + r) (f ig) * Mb * Mc

The L² von Neumann bound with the class constant and normalized norms.

theorem TrilinearHT.Auto.Lp_coeFn_finset_sum_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} (s : Finset ι) (c : ι → ℂ) (a : ι → ↥(MeasureTheory.Lp ℂ 2 μ)) (F : ι → X → ℂ) (h : ∀ i ∈ s, ↑↑(a i) =ᵐ[μ] F i) : ↑↑(∑ i ∈ s, c i • a i) =ᵐ[μ] fun (x : X) => ∑ i ∈ s, c i * F i x

The coefficient functions of a finite sum of L² classes.

theorem TrilinearHT.Auto.eLpNorm_two_le_of_bound {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hg : Measurable g) {B : ℝ} (hB : ∀ (x : ℝ), ‖g x‖ ≤ B) : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal B

theorem TrilinearHT.Auto.eLpNorm_top_le_of_bound {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℂ} (hg : Measurable g) {B : ℝ} (hB : ∀ (x : ℝ), ‖g x‖ ≤ B) : MeasureTheory.eLpNorm g ⊤ μ ≤ ENNReal.ofReal B

theorem TrilinearHT.Auto.detection_structured_slot (κ : LocalKernelClass) : ∃ (c₀ : ℕ) (D : ℝ → ℝ), 1 ≤ c₀ ∧ QuasipolynomialBound D ∧ ∀ {a₀ r : ℝ}, 0 < r → ∀ {w : ℝ × ℝ → ℂ}, IsAdmissibleLocalKernel κ a₀ r w → ∀ (f : Fin 4 → ℝ → ℂ), (∀ (j : Fin 4), Measurable (f j)) → ∀ {k jR b c : Fin 4}, k ≠ jR → k ≠ b → k ≠ c → jR ≠ b → jR ≠ c → b ≠ c → ∀ {C₁ B δ' τ : ℝ}, 0 ≤ C₁ → 1 ≤ B → 0 < τ → τ < 1 / 2 → MeasureTheory.eLpNorm (f jR) 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁ → (∀ (x : ℝ), ‖f k x‖ ≤ B) → (∀ (x : ℝ), ‖f b x‖ ≤ B) → (∀ (x : ℝ), ‖f c x‖ ≤ B) → 4 * (vonNeumannConst κ * C₁ * B ^ 3 * τ) ≤ δ' → δ' < ‖localProgressionForm r w f‖ → ∃ (d : ℕ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ (D (1 / τ)) A ∧ IsBoundedQuadraticChart A ∧ δ' / (2 * B * max 1 (D (1 / τ))) < ‖localProgressionForm r w (Function.update f k (quadraticChartAtom A))‖

Blueprint lem:detection, line 1471, one decomposition step: decomposing a B-bounded input by eq:decomp at accuracy τ and discarding both errors by eq:von-neumann leaves a single bounded atom in its slot with a large form.

def TrilinearHT.Auto.QPLe (Y : ℝ) (K : ℕ) (a : ℝ) : Prop

The quasipolynomial budget shape a ≤ exp(K Y^K) used in lem:detection.

Equations

• TrilinearHT.Auto.QPLe Y K a = (a ≤ Real.exp (↑K * Y ^ K))

theorem TrilinearHT.Auto.QPLe.mono {Y a : ℝ} {K L : ℕ} (hY : 1 ≤ Y) (hKL : K ≤ L) (h : QPLe Y K a) : QPLe Y L a

theorem TrilinearHT.Auto.QPLe.of_le {Y a b : ℝ} {K : ℕ} (hab : a ≤ b) (h : QPLe Y K b) : QPLe Y K a

theorem TrilinearHT.Auto.QPLe.one_le {Y : ℝ} {K : ℕ} (hY : 1 ≤ Y) : QPLe Y K 1

theorem TrilinearHT.Auto.QPLe.mul {Y a b : ℝ} {K L : ℕ} (hY : 1 ≤ Y) (hb0 : 0 ≤ b) (ha : QPLe Y K a) (hb : QPLe Y L b) : QPLe Y (K + L) (a * b)

theorem TrilinearHT.Auto.QPLe.pow {Y a : ℝ} {K : ℕ} (hY : 1 ≤ Y) (ha0 : 0 ≤ a) (ha : QPLe Y K a) (n : ℕ) : QPLe Y (n * K + K) (a ^ n)

theorem TrilinearHT.Auto.QPLe.const {Y : ℝ} (hY : 1 ≤ Y) (c : ℝ) : QPLe Y ⌈c⌉₊ c

theorem TrilinearHT.Auto.QPLe.log_le {Y a : ℝ} {K : ℕ} (ha0 : 0 < a) (h : QPLe Y K a) : Real.log a ≤ ↑K * Y ^ K

theorem TrilinearHT.Auto.QPLe.compose {Y a : ℝ} {K : ℕ} (hY : 1 ≤ Y) {D : ℕ} (ha1 : 1 ≤ a) (ha : QPLe Y K a) : QPLe Y (D * (1 + K) ^ D + K * D) (Real.exp (↑D * (1 + Real.log a) ^ D))

Composition with a quasipolynomial function of log a.

theorem TrilinearHT.Auto.real_integral_affine (G : ℝ → ℂ) {c : ℝ} (u : ℝ) : ∫ (t : ℝ), G (u + c * t) = ↑|c⁻¹| * ∫ (s : ℝ), G s

theorem TrilinearHT.Auto.real_progression_pair_integral {F G : ℝ → ℂ} (hFm : Measurable F) (hGm : Measurable G) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hG : MeasureTheory.Integrable G MeasureTheory.volume) {i j : ℝ} (hij : i ≠ j) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => F (z.1 + i * z.2) * G (z.1 + j * z.2)) MeasureTheory.volume ∧ ∫ (z : ℝ × ℝ), F (z.1 + i * z.2) * G (z.1 + j * z.2) = (↑|(j - i)⁻¹| * ∫ (u : ℝ), F u) * ∫ (v : ℝ), G v

Two distinct real progression slots: the complex form of real_progression_pair_lintegral, with Jacobian j - i.

theorem TrilinearHT.Auto.localProgression_absolute_le_slots {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (j : Fin 4), Measurable (f j)) {a b c d : Fin 4} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (pa pb pc pd : ENNReal) (ha : 1 ≤ pa) (hb : 1 ≤ pb) (hc : 1 ≤ pc) (hd : 1 ≤ pd) (hsum : pa.toReal⁻¹ + pb.toReal⁻¹ + pc.toReal⁻¹ + pd.toReal⁻¹ ≤ 2) : ENNReal.ofReal r⁻¹ ^ 2 * ∫⁻ (z : ℝ × ℝ), ‖w z * ∏ j : Fin 4, f j (realProgressionCoordinate j z)‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * (MeasureTheory.eLpNorm (f a) pa (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f b) pb (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f c) pc (normalizedIntervalMeasure a₀ r) * MeasureTheory.eLpNorm (f d) pd (normalizedIntervalMeasure a₀ r))

eq:absolute for the positive local form, with exponents assigned to four distinct slots.

noncomputable def TrilinearHT.Auto.separatedLocalForm (r : ℝ) (w : ℝ × ℝ → ℂ) (Q : ℝ → ℂ) (a b : Fin 4) (Fa Fb : ℝ → ℂ) : ℂ

The separated single-scale form r⁻² ∫ w Q(t) F_a(y_a) F_b(y_b).

Equations

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

theorem TrilinearHT.Auto.localProgressionForm_pair_expansion {κ : LocalKernelClass} {a₀ r : ℝ} (hr : 0 < r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a₀ r w) {a i k b : Fin 4} (hai : a ≠ i) (hak : a ≠ k) (hab : a ≠ b) (hik : i ≠ k) (hib : i ≠ b) (hkb : k ≠ b) {R v φ φ' : ℝ → ℂ} (hRm : Measurable R) (hvm : Measurable v) {C₁ : ℝ} (hC₁ : 0 ≤ C₁) (hR : MeasureTheory.eLpNorm R 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C₁) (hv : MeasureTheory.eLpNorm v 2 (normalizedIntervalMeasure a₀ r) ≤ 1) {τ : Type u_1} [Countable τ] (cf : τ → ℂ) (ψa ψb Q : τ → ℝ → ℂ) (hψam : ∀ (q : τ), Measurable (ψa q)) (hψbm : ∀ (q : τ), Measurable (ψb q)) (hQm : ∀ (q : τ), Measurable (Q q)) (hψab : ∀ (q : τ) (y : ℝ), ‖ψa q y‖ ≤ 1) (hψbb : ∀ (q : τ) (y : ℝ), ‖ψb q y‖ ≤ 1) (hQb : ∀ (q : τ) (y : ℝ), ‖Q q y‖ ≤ 1) (hcs : Summable fun (q : τ) => ‖cf q‖) (hexp : ∀ (x t : ℝ), HasSum (fun (q : τ) => cf q * ψa q (x + ↑↑a * t) * ψb q (x + ↑↑b * t) * Q q t) (φ (x + ↑↑i * t) * φ' (x + ↑↑k * t))) (f : Fin 4 → ℝ → ℂ) (hfa : f a = R) (hfi : f i = φ) (hfk : f k = φ') (hfb : f b = v) : HasSum (fun (q : τ) => cf q * separatedLocalForm r w (Q q) a b (fun (y : ℝ) => R y * ψa q y) fun (y : ℝ) => v y * ψb q y) (localProgressionForm r w f) ∧ ∀ (q : τ), ‖separatedLocalForm r w (Q q) a b (fun (y : ℝ) => R y * ψa q y) fun (y : ℝ) => v y * ψb q y‖ ≤ localFormUniformConstant κ * C₁

Blueprint lem:detection, line 1473: expanding an atom pair by lem:separation expands the local form into separated forms, each bounded by the absolute estimate.

theorem TrilinearHT.Auto.exists_large_retained_term {τ : Type u_1} (cf X : τ → ℂ) (size : τ → ℝ) {E M δ T : ℝ} (hcs : Summable fun (q : τ) => ‖cf q‖) (hE : ∑' (q : τ), ‖cf q‖ ≤ E) (hE0 : 0 < E) (hX : ∀ (q : τ), ‖X q‖ ≤ M) (hM : 0 ≤ M) (hδ0 : 0 ≤ δ) (htail : (∑' (q : τ), if T ≤ size q then ‖cf q‖ else 0) * M ≤ δ / 2) (hδ : δ < ‖∑' (q : τ), cf q * X q‖) : ∃ (q : τ), size q < T ∧ δ / (2 * E) < ‖X q‖

Blueprint lem:detection, line 1473: after truncating the shells, some retained term of a large absolutely convergent expansion is large.

theorem TrilinearHT.Auto.memLp_Icc_of_normalized {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hg : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≠ ⊤) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Icc a₀ (a₀ + r)))

theorem TrilinearHT.Auto.sqrt_normalized_Icc_le_of_eLpNorm {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} {C : ℝ} (hC : 0 ≤ C) (hg : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C) : √(r⁻¹ * ∫ (y : ℝ) in Set.Icc a₀ (a₀ + r), ‖g y‖ ^ 2) ≤ C

theorem TrilinearHT.Auto.integral_indicator_norm_le_of_eLpNorm {a₀ r : ℝ} (hr : 0 < r) {g : ℝ → ℂ} (hgm : Measurable g) {C : ℝ} (hC : 0 ≤ C) (hg : MeasureTheory.eLpNorm g 2 (normalizedIntervalMeasure a₀ r) ≤ ENNReal.ofReal C) : MeasureTheory.Integrable ((Set.Icc a₀ (a₀ + r)).indicator g) MeasureTheory.volume ∧ ∫ (y : ℝ), ‖(Set.Icc a₀ (a₀ + r)).indicator g y‖ ≤ r * C

Normalized L¹ control of a normalized L² input on the closed cell.

theorem TrilinearHT.Auto.real_progression_pair_integral_norm {F G : ℝ → ℂ} (hFm : Measurable F) (hGm : Measurable G) (hF : MeasureTheory.Integrable F MeasureTheory.volume) (hG : MeasureTheory.Integrable G MeasureTheory.volume) {i j : ℝ} (hij : i ≠ j) : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => ‖F (z.1 + i * z.2)‖ * ‖G (z.1 + j * z.2)‖) MeasureTheory.volume ∧ ∫ (z : ℝ × ℝ), ‖F (z.1 + i * z.2)‖ * ‖G (z.1 + j * z.2)‖ = (|(j - i)⁻¹| * ∫ (u : ℝ), ‖F u‖) * ∫ (v : ℝ), ‖G v‖

The positive form of real_progression_pair_integral.

theorem TrilinearHT.Auto.one_le_abs_fin_sub {a b : Fin 4} (hab : a ≠ b) : 1 ≤ |↑↑b - ↑↑a|

theorem TrilinearHT.Auto.abs_fin_four_le (a : Fin 4) : |↑↑a| ≤ 3

theorem TrilinearHT.Auto.plateau_lipschitz {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) {Kψ : ℕ} (hder : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i ψ x| ≤ (↑Kψ * (↑i + 1)) ^ (Kψ * (i + 1))) (u v : ℝ) : |ψ v - ψ u| ≤ (↑Kψ * 2) ^ (Kψ * 2) * |v - u|

A plateau cutoff is Lipschitz with a fixed constant.

theorem TrilinearHT.Auto.plateau_integrable {ψ : ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψ0 : ∀ (x : ℝ), 2 ≤ |x| → ψ x = 0) : MeasureTheory.Integrable ψ MeasureTheory.volume