Section 7: A finite inverse theorem with a complete proof

This file was automatically generated by Claude.

Formalization of blueprint Section 7, "A finite inverse theorem with a complete proof" (sec:finite-inverse, lines 929-1163) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.finiteFourier_trilinear_identity {q : ℕ} [NeZero q] (F B A : ZMod q → ℂ) : (finiteAverage fun (u : ZMod q) => finiteAverage fun (t : ZMod q) => F u * B t * A (u + t)) = ∑ ξ : ZMod q, finiteFourier F (-ξ) * finiteFourier B (-ξ) * finiteFourier A ξ

theorem TrilinearHT.Auto.finiteFourier_trilinear_select {q : ℕ} [NeZero q] (F B A : ZMod q → ℂ) : ∃ (ξ : ZMod q), ‖finiteAverage fun (u : ZMod q) => finiteAverage fun (t : ZMod q) => F u * B t * A (u + t)‖ ≤ ‖finiteFourier F ξ‖ * √(uniformMean fun (t : ZMod q) => ‖B t‖ ^ 2) * √(uniformMean fun (u : ZMod q) => ‖A u‖ ^ 2)

theorem TrilinearHT.Auto.finite_weighted_trilinear_extract {q : ℕ} [NeZero q] (w : ZMod q → ℝ) (hw0 : ∀ (u : ZMod q), 0 ≤ w u) (hw1 : ∀ (u : ZMod q), w u ≤ 1) {β η : ℝ} (hβ : 0 < β) (hmass : (Finset.univ.expect fun (u : ZMod q) => w u) = β) (b c A : ZMod q → ℂ) (hc : ∀ (u : ZMod q), ‖c u‖ ≤ 1) (hA : ∀ (u : ZMod q), ‖A u‖ ≤ 1) (hcorr : η ≤ ‖Finset.univ.expect fun (u : ZMod q) => Finset.univ.expect fun (t : ZMod q) => ↑(w u / β) * b u * (↑(w t / β) * c t) * A (u + t)‖) : ∃ (ξ : ZMod q), η * β * √β ≤ ‖Finset.univ.expect fun (u : ZMod q) => ↑(w u) * b u * ZMod.stdAddChar (-(ξ * u))‖

theorem TrilinearHT.Auto.cyclicBohrMeasure_mean_one {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (hβ : 0 < cyclicBohrMass b S r) : (Finset.univ.expect fun (x : ZMod q) => cyclicBohrMeasure b S r x) = 1

theorem TrilinearHT.Auto.cyclicBohrMeasure_nonneg {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (S : Finset (ZMod q)) (r : ℝ) (hβ : 0 < cyclicBohrMass b S r) (x : ZMod q) : 0 ≤ cyclicBohrMeasure b S r x

Local symmetry of graph frequencies

theorem TrilinearHT.Auto.graphBohrSet_mono {q : ℕ} [NeZero q] {S T : Finset (ZMod q)} (hST : S ⊆ T) {r ρ : ℝ} (hr : r ≤ ρ) : graphBohrSet T r ⊆ graphBohrSet S ρ

theorem TrilinearHT.Auto.graphBohrSet_add {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {r ρ : ℝ} {x y : ZMod q} (hx : x ∈ graphBohrSet S r) (hy : y ∈ graphBohrSet S ρ) : x + y ∈ graphBohrSet S (r + ρ)

theorem TrilinearHT.Auto.graphBohrSet_neg {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {r : ℝ} {x : ZMod q} (hx : x ∈ graphBohrSet S r) : -x ∈ graphBohrSet S r

theorem TrilinearHT.Auto.graphBohrSet_sub {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {r ρ : ℝ} {x y : ZMod q} (hx : x ∈ graphBohrSet S r) (hy : y ∈ graphBohrSet S ρ) : x - y ∈ graphBohrSet S (r + ρ)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.graphBohrWeight {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) : ℝ

Smooth Bohr weight for the local graph model.

Equations

• TrilinearHT.Auto.graphBohrWeight b S r x = TrilinearHT.Auto.cyclicBohrWeight b S r x

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.graphBohrMass {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) : ℝ

Uniform mass of the smoothed graph Bohr weight.

Equations

• TrilinearHT.Auto.graphBohrMass b S r = TrilinearHT.Auto.cyclicBohrMass b S r

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.graphBohrMeasure {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) : ℝ

Graph Bohr weight divided by its uniform mass.

Equations

• TrilinearHT.Auto.graphBohrMeasure b S r x = TrilinearHT.Auto.cyclicBohrMeasure b S r x

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.graphBohrNorm {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (x : ZMod q) : ℝ

Largest character distance among the frequencies in S.

Equations

• TrilinearHT.Auto.graphBohrNorm S x = TrilinearHT.Auto.cyclicBohrNorm S x

theorem TrilinearHT.Auto.graphBohrWeight_bounds {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (S : Finset (ZMod q)) (r : ℝ) (x : ZMod q) : 0 ≤ graphBohrWeight b S r x ∧ graphBohrWeight b S r x ≤ 1

theorem TrilinearHT.Auto.graphBohrWeight_eq_zero_of_notMem {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → b x = 0) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (x : ZMod q) (hx : x ∉ graphBohrSet S r) : graphBohrWeight b S r x = 0

theorem TrilinearHT.Auto.graphBohrMass_bounds {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → b x = 1) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) : (r / 6) ^ S.card ≤ graphBohrMass b S r ∧ graphBohrMass b S r ≤ 1

theorem TrilinearHT.Auto.graphBohrMeasure_mean_one {q : ℕ} [NeZero q] (b : ℝ → ℝ) (S : Finset (ZMod q)) (r : ℝ) (hβ : 0 < graphBohrMass b S r) : (Finset.univ.expect fun (x : ZMod q) => graphBohrMeasure b S r x) = 1

theorem TrilinearHT.Auto.graphBohrNorm_le_of_mem {q : ℕ} [NeZero q] (S : Finset (ZMod q)) {r : ℝ} (hr : 0 ≤ r) {x : ZMod q} (hx : x ∈ graphBohrSet S r) : graphBohrNorm S x ≤ r

theorem TrilinearHT.Auto.localSymmetryInnerRadius_bounds {C r ζ : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hζ : 0 < ζ) (d : ℕ) : 0 < localSymmetryInnerRadius C d r ζ ∧ localSymmetryInnerRadius C d r ζ ≤ r / 100 ∧ 2 * C * ↑d * localSymmetryInnerRadius C d r ζ / r ≤ ζ ^ 2 / 2

theorem TrilinearHT.Auto.graphBohrMass_pos {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → b x = 1) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) : 0 < graphBohrMass b S r

theorem TrilinearHT.Auto.graphBohrMeasure_nonneg {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hb : ∀ (x : ℝ), 0 ≤ b x) (S : Finset (ZMod q)) (r : ℝ) (hβ : 0 < graphBohrMass b S r) (x : ZMod q) : 0 ≤ graphBohrMeasure b S r x

theorem TrilinearHT.Auto.graphBohrMeasure_eq_zero_of_notMem {q : ℕ} [NeZero q] (b : ℝ → ℝ) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → b x = 0) (S : Finset (ZMod q)) {r : ℝ} (hr : 0 < r) (x : ZMod q) (hx : x ∉ graphBohrSet S r) : graphBohrMeasure b S r x = 0

theorem TrilinearHT.Auto.localSymmetryInnerRadius_domain {C r ζ ρ : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hζ : 0 < ζ) (d : ℕ) (hrρ : r ≤ ρ / 100) : r + 2 * localSymmetryInnerRadius C d r ζ < ρ ∧ 8 * localSymmetryInnerRadius C d r ζ < ρ ∧ 3 * localSymmetryInnerRadius C d r ζ < r

theorem TrilinearHT.Auto.finite_weighted_shift_average {G : Type u_1} [Fintype G] [AddCommGroup G] (μ : G → ℝ) (hμ : (Finset.univ.expect fun (u : G) => μ u) = 1) (F : G → ℂ) : (Finset.univ.expect fun (y : G) => Finset.univ.expect fun (u : G) => ↑(μ u) * F (y + u)) = Finset.univ.expect fun (x : G) => F x

Averaging all translates of a normalized weight preserves uniform averages.

theorem TrilinearHT.Auto.finite_weighted_translation_localization {G : Type u_1} [Fintype G] [AddCommGroup G] (μ : G → ℝ) (hμ : (Finset.univ.expect fun (u : G) => μ u) = 1) (F : G → G → ℂ) {ζ : ℝ} (hζ : ζ ≤ ‖Finset.univ.expect fun (h : G) => Finset.univ.expect fun (x : G) => F h x‖) : ∃ (y : G), ζ ≤ ‖Finset.univ.expect fun (h : G) => Finset.univ.expect fun (u : G) => ↑(μ u) * F h (y + u)‖

Some weighted translate retains the magnitude of a two-variable uniform correlation.

noncomputable def TrilinearHT.Auto.graphLocalCorrelation {q : ℕ} [NeZero q] (w : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) : ℂ

Initial correlation in the local-symmetry argument.

Equations

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

noncomputable def TrilinearHT.Auto.graphLocalizedCorrelation {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) : ℂ

Correlation after localizing the spatial variable by a normalized weight.

Equations

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

theorem TrilinearHT.Auto.graph_correlation_localization {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hμ : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) {ζ : ℝ} (hζ : ζ ≤ ‖graphLocalCorrelation w M a b c‖) : ∃ (a' : ZMod q → ℂ) (b' : ZMod q → ℂ) (c' : ZMod q → ℂ), (∀ (x : ZMod q), ‖a' x‖ ≤ 1) ∧ (∀ (x : ZMod q), ‖b' x‖ ≤ 1) ∧ (∀ (x : ZMod q), ‖c' x‖ ≤ 1) ∧ ζ ≤ ‖graphLocalizedCorrelation w μ M a' b' c'‖

The selected translate is absorbed into bounded functions without changing the graph frequency.

theorem TrilinearHT.Auto.finite_weighted_complex_cauchy_schwarz {I : Type u_1} [Fintype I] (w : I → ℝ) (hw : ∀ (i : I), 0 ≤ w i) (hmass : (Finset.univ.expect fun (i : I) => w i) ≤ 1) (c F : I → ℂ) (hc : ∀ (i : I), ‖c i‖ ≤ 1) : ‖Finset.univ.expect fun (i : I) => ↑(w i) * c i * F i‖ ^ 2 ≤ Finset.univ.expect fun (i : I) => w i * ‖F i‖ ^ 2

Weighted Cauchy-Schwarz for a nonnegative weight of uniform mass at most one.

noncomputable def TrilinearHT.Auto.graphLocalizedSquare {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) : ℝ

The real nonnegative square left by the first local-symmetry Cauchy-Schwarz step.

Equations

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

theorem TrilinearHT.Auto.graphLocalizedSquare_nonneg {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hw : ∀ (h : ZMod q), 0 ≤ w h) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) : 0 ≤ graphLocalizedSquare w μ M a b

theorem TrilinearHT.Auto.graph_localized_cauchy_schwarz {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hw : ∀ (h : ZMod q), 0 ≤ w h) (hmass : (Finset.univ.expect fun (h : ZMod q) => w h) ≤ 1) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) (hc : ∀ (h : ZMod q), ‖c h‖ ≤ 1) {ζ : ℝ} (hζ : 0 ≤ ζ) (hcorr : ζ ≤ ‖graphLocalizedCorrelation w μ M a b c‖) : ζ ^ 2 ≤ graphLocalizedSquare w μ M a b

The first weighted Cauchy-Schwarz inequality in the source local-symmetry proof.

theorem TrilinearHT.Auto.graphLocalizedSquare_expansion {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) : ↑(graphLocalizedSquare w μ M a b) = Finset.univ.expect fun (h : ZMod q) => Finset.univ.expect fun (u : ZMod q) => Finset.univ.expect fun (v : ZMod q) => ↑(w h) * ↑(μ u) * ↑(μ v) * b u * (starRingEnd ℂ) (b v) * a (u + h) * (starRingEnd ℂ) (a (v + h)) * ZMod.stdAddChar (-(2 * M h * (u - v)))

Exact complex expansion of the first square, with the differenced frequency phase.

def TrilinearHT.Auto.graphAlternating {q : ℕ} (M : ZMod q → ZMod q) (u v : ZMod q) : ZMod q

The alternating graph-frequency expression, before applying the circle embedding.

Equations

• TrilinearHT.Auto.graphAlternating M u v = M u * v - M v * u

noncomputable def TrilinearHT.Auto.graphAlternatingPhase {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (u v : ZMod q) : UnitAddCircle

Circle-valued alternating phase associated with the local frequency map.

Equations

• TrilinearHT.Auto.graphAlternatingPhase M u v = ZMod.toAddCircle (TrilinearHT.Auto.graphAlternating M u v)

theorem TrilinearHT.Auto.graph_local_additive_three {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (M : ZMod q → ZMod q) {r s ρ : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) (hρ : r + 2 * s ≤ ρ) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) {h u v : ZMod q} (hh : h ∈ graphBohrSet S r) (hu : u ∈ graphBohrSet S s) (hv : v ∈ graphBohrSet S s) : M h = M (h + (u + v)) - M u - M v

Local additivity suffices to reconstruct the outer frequency after the three-term shift.

noncomputable def TrilinearHT.Auto.graphLocalAmplitude {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (z u : ZMod q) : ℂ

The bounded amplitude obtained after writing z=h+u+v.

Equations

• TrilinearHT.Auto.graphLocalAmplitude M a b z u = b u * (starRingEnd ℂ) (a (z - u)) * ZMod.stdAddChar (2 * M u * u - 2 * M z * u)

theorem TrilinearHT.Auto.graph_local_phase_identity {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (h u v : ZMod q) (hM : M h = M (h + (u + v)) - M u - M v) : b u * (starRingEnd ℂ) (b v) * a (u + h) * (starRingEnd ℂ) (a (v + h)) * ZMod.stdAddChar (-(2 * M h * (u - v))) = graphLocalAmplitude M a b (h + (u + v)) u * (starRingEnd ℂ) (graphLocalAmplitude M a b (h + (u + v)) v) * ZMod.stdAddChar (-(2 * graphAlternating M u v))

Exact algebraic alternating-phase identity on the locally additive domain.

noncomputable def TrilinearHT.Auto.graphSymmetryExpression {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) : ℂ

The reindexed weighted alternating-phase average in the source symmetry argument.

Equations

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

theorem TrilinearHT.Auto.graphLocalizedSquare_symmetry_change {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) {r s ρ : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) (hρ : r + 2 * s ≤ ρ) (hw : ∀ (h : ZMod q), w h ≠ 0 → h ∈ graphBohrSet S r) (hμ : ∀ (u : ZMod q), μ u ≠ 0 → u ∈ graphBohrSet S s) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) : ↑(graphLocalizedSquare w μ M a b) = graphSymmetryExpression w μ M a b

Reindexing is valid because every nonzero weighted term lies inside the additive domain.

theorem TrilinearHT.Auto.graphLocalAmplitude_norm_le {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (z u : ZMod q) : ‖graphLocalAmplitude M a b z u‖ ≤ 1

noncomputable def TrilinearHT.Auto.graphSymmetryKernel {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (z u v : ZMod q) : ℂ

The unit-bounded kernel of the alternating-phase correlation.

Equations

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

theorem TrilinearHT.Auto.graphSymmetryKernel_norm_le {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (z u v : ZMod q) : ‖graphSymmetryKernel M a b z u v‖ ≤ 1

theorem TrilinearHT.Auto.finite_weighted_pair_norm_le {I : Type u_1} [Fintype I] (μ : I → ℝ) (hμ : ∀ (i : I), 0 ≤ μ i) (hmass : (Finset.univ.expect fun (i : I) => μ i) = 1) (F : I → I → ℂ) {A : ℝ} (hF : ∀ (u v : I), μ u ≠ 0 → μ v ≠ 0 → ‖F u v‖ ≤ A) : ‖Finset.univ.expect fun (u : I) => Finset.univ.expect fun (v : I) => ↑(μ u) * ↑(μ v) * F u v‖ ≤ A

A two-variable normalized weighted average obeys a bound valid on the weight's support.

theorem TrilinearHT.Auto.finite_weighted_correlation_select {I : Type u_1} [Fintype I] (w : I → ℝ) (hw : ∀ (i : I), 0 ≤ w i) (hmass : (Finset.univ.expect fun (i : I) => w i) ≤ 1) (F : I → ℂ) {η : ℝ} (hη : 0 < η) (hcorr : η ≤ ‖Finset.univ.expect fun (i : I) => ↑(w i) * F i‖) : ∃ (i : I), w i ≠ 0 ∧ η ≤ ‖F i‖

A positive weighted correlation is witnessed at a point carrying nonzero weight.

theorem TrilinearHT.Auto.graphBohrWeight_pair_translation {q : ℕ} [NeZero q] (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (x : ℝ), 0 ≤ b x) (hb1 : ∀ (x : ℝ), b x ≤ 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → b x = 0) (S : Finset (ZMod q)) {r s : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hs : 0 ≤ s) (z u v : ZMod q) (hu : u ∈ graphBohrSet S s) (hv : v ∈ graphBohrSet S s) : |graphBohrWeight b S r (z - u - v) - graphBohrWeight b S r z| ≤ 2 * max (↑L) 1 * ↑S.card * s / r

Pairwise shifts of inner Bohr points incur the source weight-replacement error.

noncomputable def TrilinearHT.Auto.graphSymmetryFixedCorrelation {q : ℕ} [NeZero q] (μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (z : ZMod q) : ℂ

The inner alternating-phase correlation at a fixed outer parameter.

Equations

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

noncomputable def TrilinearHT.Auto.graphSymmetryWeightedCorrelation {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) : ℂ

Outer-weighted average of the fixed-shift graph-symmetry correlation.

Equations

• TrilinearHT.Auto.graphSymmetryWeightedCorrelation w μ M a b = Finset.univ.expect fun (z : ZMod q) => ↑(w z) * TrilinearHT.Auto.graphSymmetryFixedCorrelation μ M a b z

theorem TrilinearHT.Auto.graph_symmetry_weight_error {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hμ : ∀ (u : ZMod q), 0 ≤ μ u) (hμmass : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) {ε : ℝ} (htrans : ∀ (z u v : ZMod q), μ u ≠ 0 → μ v ≠ 0 → |w (z - u - v) - w z| ≤ ε) : ‖graphSymmetryExpression w μ M a b - graphSymmetryWeightedCorrelation w μ M a b‖ ≤ ε

Replacing the shifted outer weight costs at most its uniform variation on the inner support.

theorem TrilinearHT.Auto.graph_symmetry_weight_replacement_select {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hw : ∀ (z : ZMod q), 0 ≤ w z) (hwmass : (Finset.univ.expect fun (z : ZMod q) => w z) ≤ 1) (hμ : ∀ (u : ZMod q), 0 ≤ μ u) (hμmass : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) {ζ ε : ℝ} (hζ : 0 < ζ) (hε : ε ≤ ζ ^ 2 / 2) (hsq : ζ ^ 2 ≤ graphLocalizedSquare w μ M a b) (hchange : ↑(graphLocalizedSquare w μ M a b) = graphSymmetryExpression w μ M a b) (htrans : ∀ (z u v : ZMod q), μ u ≠ 0 → μ v ≠ 0 → |w (z - u - v) - w z| ≤ ε) : ∃ (z : ZMod q), w z ≠ 0 ∧ ζ ^ 2 / 2 ≤ ‖graphSymmetryFixedCorrelation μ M a b z‖

The weight replacement leaves a large fixed-parameter correlation on the outer support.

theorem TrilinearHT.Auto.graph_bohr_symmetry_select {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S : Finset (ZMod q)) {r s ρ ζ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hs : 0 < s) (hssmall : s < 1 / 8) (hρ : r + 2 * s ≤ ρ) (hζ : 0 < ζ) (htol : 2 * max (↑L) 1 * ↑S.card * s / r ≤ ζ ^ 2 / 2) (M : ZMod q → ZMod q) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (hsq : ζ ^ 2 ≤ graphLocalizedSquare (graphBohrWeight cutoff S r) (graphBohrMeasure cutoff S s) M a b) : ∃ (z : ZMod q), graphBohrWeight cutoff S r z ≠ 0 ∧ z ∈ graphBohrSet S r ∧ ζ ^ 2 / 2 ≤ ‖graphSymmetryFixedCorrelation (graphBohrMeasure cutoff S s) M a b z‖

Source weight replacement and supported selection, specialized to the actual smooth Bohr weights.

theorem TrilinearHT.Auto.finite_expect_cycle_three {I : Type u_1} {J : Type u_2} {K : Type u_3} [Fintype I] [Fintype J] [Fintype K] (f : I → J → K → ℂ) : (Finset.univ.expect fun (i : I) => Finset.univ.expect fun (j : J) => Finset.univ.expect fun (k : K) => f i j k) = Finset.univ.expect fun (j : J) => Finset.univ.expect fun (k : K) => Finset.univ.expect fun (i : I) => f i j k

theorem TrilinearHT.Auto.finite_weighted_kernel_square {I : Type u_1} [Fintype I] (μ : I → ℝ) (A : I → ℂ) (K : I → I → ℂ) : ↑(Finset.univ.expect fun (u : I) => μ u * ‖Finset.univ.expect fun (v : I) => ↑(μ v) * (starRingEnd ℂ) (A v) * K u v‖ ^ 2) = Finset.univ.expect fun (v : I) => Finset.univ.expect fun (v' : I) => ↑(μ v) * ↑(μ v') * (starRingEnd ℂ) (A v) * A v' * Finset.univ.expect fun (u : I) => ↑(μ u) * K u v * (starRingEnd ℂ) (K u v')

Exact weighted kernel square identity after the second Cauchy-Schwarz step.

theorem TrilinearHT.Auto.finite_weighted_kernel_cauchy_schwarz {I : Type u_1} [Fintype I] (μ : I → ℝ) (hμ : ∀ (i : I), 0 ≤ μ i) (hmass : (Finset.univ.expect fun (i : I) => μ i) = 1) (A : I → ℂ) (hA : ∀ (i : I), ‖A i‖ ≤ 1) (K : I → I → ℂ) {κ : ℝ} (hκ : 0 ≤ κ) (hcorr : κ ≤ ‖Finset.univ.expect fun (u : I) => Finset.univ.expect fun (v : I) => ↑(μ u) * ↑(μ v) * A u * (starRingEnd ℂ) (A v) * K u v‖) : κ ^ 2 ≤ Finset.univ.expect fun (v : I) => Finset.univ.expect fun (v' : I) => μ v * μ v' * ‖Finset.univ.expect fun (u : I) => ↑(μ u) * K u v * (starRingEnd ℂ) (K u v')‖

A second weighted Cauchy-Schwarz removes both bounded amplitudes from a kernel correlation.

theorem TrilinearHT.Auto.graph_local_additive_sub {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (M : ZMod q → ZMod q) {s ρ : ℝ} (hs : 0 ≤ s) (hρ : 2 * s ≤ ρ) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) {v v' : ZMod q} (hv : v ∈ graphBohrSet S s) (hv' : v' ∈ graphBohrSet S s) : M (v - v') = M v - M v'

Subtraction of two inner Bohr points is compatible with the locally additive map.

theorem TrilinearHT.Auto.graph_alternating_character_difference {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (u v v' : ZMod q) (hM : M (v - v') = M v - M v') : ZMod.stdAddChar (-(2 * graphAlternating M u v)) * (starRingEnd ℂ) (ZMod.stdAddChar (-(2 * graphAlternating M u v'))) = ZMod.stdAddChar (-(2 * graphAlternating M u (v - v')))

noncomputable def TrilinearHT.Auto.graphAlternatingFourier {q : ℕ} [NeZero q] (μ : ZMod q → ℝ) (M : ZMod q → ZMod q) (v : ZMod q) : ℂ

Local Fourier coefficient of the doubled alternating phase.

Equations

• TrilinearHT.Auto.graphAlternatingFourier μ M v = Finset.univ.expect fun (u : ZMod q) => ↑(μ u) * ZMod.stdAddChar (-(2 * TrilinearHT.Auto.graphAlternating M u v))

theorem TrilinearHT.Auto.graph_symmetry_second_cauchy_schwarz {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (μ : ZMod q → ℝ) (hμ : ∀ (u : ZMod q), 0 ≤ μ u) (hμmass : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) {s ρ : ℝ} (hs : 0 ≤ s) (hρ : 2 * s ≤ ρ) (hμsupp : ∀ (u : ZMod q), μ u ≠ 0 → u ∈ graphBohrSet S s) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (a b : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (z : ZMod q) {ζ : ℝ} (hcorr : ζ ^ 2 / 2 ≤ ‖graphSymmetryFixedCorrelation μ M a b z‖) : ζ ^ 4 / 4 ≤ Finset.univ.expect fun (v : ZMod q) => Finset.univ.expect fun (v' : ZMod q) => μ v * μ v' * ‖graphAlternatingFourier μ M (v - v')‖

The source second Cauchy-Schwarz conclusion, with the exact fourth-power correlation bound.

noncomputable def TrilinearHT.Auto.weightedUpperLevel {I : Type u_1} [Fintype I] (μ θ : I → ℝ) (τ : ℝ) : Finset I

The supported upper level set used in the local-symmetry argument, blueprint lem:local-symmetry, lines 983-989.

Equations

• TrilinearHT.Auto.weightedUpperLevel μ θ τ = {i : I | μ i ≠ 0 ∧ τ ≤ θ i}

theorem TrilinearHT.Auto.finite_weighted_upper_level_mass {I : Type u_1} [Fintype I] [DecidableEq I] (μ θ : I → ℝ) (hμ : ∀ (i : I), 0 ≤ μ i) (hmass : (Finset.univ.expect fun (i : I) => μ i) = 1) (hθ : ∀ (i : I), θ i ≤ 1) {τ : ℝ} (hτ : 0 ≤ τ) (havg : 2 * τ ≤ Finset.univ.expect fun (i : I) => μ i * θ i) : τ ≤ Finset.univ.expect fun (i : I) => if i ∈ weightedUpperLevel μ θ τ then μ i else 0

A normalized weighted average at least twice the threshold gives at least the threshold of mass to its supported upper level set.

theorem TrilinearHT.Auto.finite_weighted_set_density {I : Type u_1} [Fintype I] [DecidableEq I] (μ : I → ℝ) (A : Finset I) {β τ : ℝ} (hβ : 0 < β) (hcap : ∀ (i : I), μ i ≤ 1 / β) (hmass : τ ≤ Finset.univ.expect fun (i : I) => if i ∈ A then μ i else 0) : β * τ ≤ ↑A.card / ↑(Fintype.card I)

A pointwise density cap converts normalized weighted mass to counting density.

theorem TrilinearHT.Auto.graphAlternatingFourier_norm_le {q : ℕ} [NeZero q] (μ : ZMod q → ℝ) (hμ : ∀ (u : ZMod q), 0 ≤ μ u) (hmass : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) (v : ZMod q) : ‖graphAlternatingFourier μ M v‖ ≤ 1

Every normalized nonnegative local Fourier coefficient has modulus at most one.

theorem TrilinearHT.Auto.graph_local_spectrum_set {q : ℕ} [NeZero q] (μ : ZMod q → ℝ) (hμ : ∀ (u : ZMod q), 0 ≤ μ u) (hmass : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) {β ζ : ℝ} (hβ : 0 < β) (hcap : ∀ (u : ZMod q), μ u ≤ 1 / β) (hζ : 0 < ζ) (M : ZMod q → ZMod q) (hcorr : ζ ^ 4 / 4 ≤ Finset.univ.expect fun (v : ZMod q) => Finset.univ.expect fun (v' : ZMod q) => μ v * μ v' * ‖graphAlternatingFourier μ M (v - v')‖) : ∃ (v' : ZMod q) (A : Finset (ZMod q)), μ v' ≠ 0 ∧ A.Nonempty ∧ (ζ ^ 4 / 8 ≤ Finset.univ.expect fun (v : ZMod q) => if v ∈ A then μ v else 0) ∧ β * (ζ ^ 4 / 8) ≤ ↑A.card / ↑q ∧ ∀ v ∈ A, μ v ≠ 0 ∧ ζ ^ 4 / 8 ≤ ‖graphAlternatingFourier μ M (v - v')‖

Extract the supported local spectrum with its weighted mass and ordinary density; blueprint lem:local-symmetry, lines 983-989.

theorem TrilinearHT.Auto.graphAlternatingPhase_add_left {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (x y z : ZMod q) (hM : M (x + y) = M x + M y) : graphAlternatingPhase M (x + y) z = graphAlternatingPhase M x z + graphAlternatingPhase M y z

Additivity of the alternating phase in its first argument uses only the displayed local additivity identity for the frequency map.

theorem TrilinearHT.Auto.graph_alternating_fourier_decay {q : ℕ} [NeZero q] (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (a : ℝ), 0 ≤ b a) (hb1 : ∀ (a : ℝ), b a ≤ 1) (hbone : ∀ (a : ℝ), |a| ≤ 1 / 2 → b a = 1) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) (S : Finset (ZMod q)) {r ρ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hρ : 3 * r ≤ ρ) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) {τ : ℝ} (hτ : 0 < τ) (z : ZMod q) (hcorr : τ ≤ ‖graphAlternatingFourier (graphBohrMeasure b S r) M z‖) (x : ZMod q) (hx : x ∈ graphBohrSet S r) : ‖2 • graphAlternatingPhase M x z‖ ≤ max (↑L) 1 * ↑S.card * graphBohrNorm S x / (r * graphBohrMass b S r * τ)

The exact local Fourier decay estimate for an alternating graph frequency; blueprint lem:local-symmetry, lines 990-994.

theorem TrilinearHT.Auto.graphAlternatingPhase_add_right {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (x y z : ZMod q) (hM : M (y + z) = M y + M z) : graphAlternatingPhase M x (y + z) = graphAlternatingPhase M x y + graphAlternatingPhase M x z

Additivity in the second slot of the alternating phase.

theorem TrilinearHT.Auto.graphAlternatingPhase_sub_right {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (x y z : ZMod q) (hM : M (y - z) = M y - M z) : graphAlternatingPhase M x (y - z) = graphAlternatingPhase M x y - graphAlternatingPhase M x z

Subtraction in the second slot needs only the corresponding local map identity.

theorem TrilinearHT.Auto.graph_alternating_fourfold_bound {q : ℕ} [NeZero q] (S A : Finset (ZMod q)) {r ρ E : ℝ} (hr : 0 ≤ r) (hρ : 4 * r ≤ ρ) (M : ZMod q → ZMod q) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ v ∈ graphBohrSet S ρ, u + v ∈ graphBohrSet S ρ → M (u + v) = M u + M v) (hA : A ⊆ graphBohrSet S r) (v' : ZMod q) (hv' : v' ∈ graphBohrSet S r) (x : ZMod q) (hbound : ∀ v ∈ A, ‖2 • graphAlternatingPhase M x (v - v')‖ ≤ E) (z : ZMod q) (hz : z ∈ 2 • A - 2 • A) : ‖2 • graphAlternatingPhase M x z‖ ≤ 4 * E

Four supported phase estimates extend to the double difference set, with all partial sums inside the original domain; blueprint lem:local-symmetry, lines 995-999.

theorem TrilinearHT.Auto.graph_spectrum_difference_decay {q : ℕ} [NeZero q] (b : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L b) (hb : ∀ (a : ℝ), 0 ≤ b a) (hb1 : ∀ (a : ℝ), b a ≤ 1) (hbone : ∀ (a : ℝ), |a| ≤ 1 / 2 → b a = 1) (hsupp : ∀ (a : ℝ), 1 ≤ |a| → b a = 0) (S A : Finset (ZMod q)) {r ρ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hρ : 4 * r ≤ ρ) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (hA : A ⊆ graphBohrSet S r) (v' : ZMod q) (hv' : v' ∈ graphBohrSet S r) {τ : ℝ} (hτ : 0 < τ) (hcorr : ∀ v ∈ A, τ ≤ ‖graphAlternatingFourier (graphBohrMeasure b S r) M (v - v')‖) (x : ZMod q) (hx : x ∈ graphBohrSet S r) (z : ZMod q) (hz : z ∈ 2 • A - 2 • A) : ‖2 • graphAlternatingPhase M x z‖ ≤ 4 * (max (↑L) 1 * ↑S.card / (r * graphBohrMass b S r * τ)) * graphBohrNorm S x

The local spectrum controls the alternating phase on its entire double difference set.

noncomputable def TrilinearHT.Auto.graphSymmetryRefinedRadius (ρ r ζ D : ℝ) : ℝ

A concrete radius satisfying all three shrinkage constraints in the local-symmetry proof.

Equations

• TrilinearHT.Auto.graphSymmetryRefinedRadius ρ r ζ D = ρ * r * ζ / (1000000 * (D + 1))

theorem TrilinearHT.Auto.graphSymmetryRefinedRadius_bounds {ρ r ζ D : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hD : 0 ≤ D) : 0 < graphSymmetryRefinedRadius ρ r ζ D ∧ graphSymmetryRefinedRadius ρ r ζ D ≤ ρ / 100 ∧ graphSymmetryRefinedRadius ρ r ζ D ≤ r / 100 ∧ 1000000 * D * graphSymmetryRefinedRadius ρ r ζ D ≤ ζ

The product radius is positive, small in each domain, and small enough for the phase bound.

theorem TrilinearHT.Auto.graphSymmetryRefinedRadius_log {ρ r ζ D : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hζ : 0 < ζ) (hD : 0 ≤ D) : Real.log (1 / graphSymmetryRefinedRadius ρ r ζ D) = Real.log (1 / ρ) + Real.log (1 / r) + Real.log (1 / ζ) + Real.log 1000000 + Real.log (D + 1)

Exact logarithmic cost of the explicit refined radius.

theorem TrilinearHT.Auto.graph_symmetry_dense_subdomain {q : ℕ} [NeZero q] (S A : Finset (ZMod q)) (hA : A.Nonempty) {r ζ D : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hD : 0 ≤ D) : ∃ (T : Finset (ZMod q)) (s : ℝ), S ⊆ T ∧ 1 ∈ T ∧ 0 < s ∧ s ≤ r / 100 ∧ 1000000 * D * s ≤ ζ ∧ graphBohrSet T s ⊆ 2 • A - 2 • A ∧ ↑T.card + Real.log (1 / s) ≤ ↑S.card + 10 ^ 20 * (1 + Real.log (1 / (↑A.card / ↑q))) ^ 4 + Real.log (1 / r) + Real.log (1 / ζ) + Real.log 1000000 + Real.log (D + 1)

Dense Bogolyubov followed by an explicit radius shrinkage, preserving the original frequencies and recording the complete rank/logarithmic cost.

theorem TrilinearHT.Auto.graphBohrSet_doubling {q : ℕ} [NeZero q] (hq : Odd q) (T : Finset (ZMod q)) (r : ℝ) : graphBohrSet (Finset.image (fun (t : ZMod q) => 2⁻¹ * t) T) r = Finset.image (fun (u : ZMod q) => 2 * u) (graphBohrSet T r)

In odd cyclic groups, doubling a Bohr domain divides its frequencies by two. Here doubling is an image, not the sum of two independently chosen points.

theorem TrilinearHT.Auto.graphAlternatingPhase_double {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (u v : ZMod q) (hu : M (2 * u) = 2 * M u) (hv : M (2 * v) = 2 * M v) : graphAlternatingPhase M (2 * u) (2 * v) = 4 • graphAlternatingPhase M u v

Local doubling in each argument quadruples the circle-valued alternating phase.

theorem TrilinearHT.Auto.graph_symmetry_doubling_domain {q : ℕ} [NeZero q] (hq : Odd q) (S T : Finset (ZMod q)) (hST : S ⊆ T) {r s ρ D : ℝ} (hsr : s ≤ r) (hρ : 2 * r ≤ ρ) (hr : 0 ≤ r) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (hphase : ∀ u ∈ graphBohrSet T s, ∀ v ∈ graphBohrSet T s, ‖2 • graphAlternatingPhase M u v‖ ≤ 4 * D * s) : ∃ (S' : Finset (ZMod q)), S ⊆ S' ∧ S'.card ≤ S.card + T.card ∧ ∀ x ∈ graphBohrSet S' s, ∀ y ∈ graphBohrSet S' s, ‖graphAlternatingPhase M x y‖ ≤ 8 * D * s

Doubling the small domain controls the phase itself, without dividing a circle norm; blueprint lem:local-symmetry, lines 1008-1013.

theorem TrilinearHT.Auto.graph_symmetry_from_spectrum {q : ℕ} [NeZero q] (hq : Odd q) (S A : Finset (ZMod q)) (hA : A.Nonempty) {r ρ ζ D : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (hρ : 2 * r ≤ ρ) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hD : 0 ≤ D) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (hphase : ∀ u ∈ graphBohrSet S r, ∀ v ∈ 2 • A - 2 • A, ‖2 • graphAlternatingPhase M u v‖ ≤ 4 * D * graphBohrNorm S u) : ∃ (S' : Finset (ZMod q)) (s : ℝ), S ⊆ S' ∧ 0 < s ∧ s < r ∧ (∀ x ∈ graphBohrSet S' s, ∀ y ∈ graphBohrSet S' s, ‖graphAlternatingPhase M x y‖ ≤ ζ / 1000) ∧ ↑S'.card + Real.log (1 / s) ≤ 2 * ↑S.card + 10 ^ 20 * (1 + Real.log (1 / (↑A.card / ↑q))) ^ 4 + Real.log (1 / r) + Real.log (1 / ζ) + Real.log 1000000 + Real.log (D + 1)

The dense spectrum estimate yields a smaller symmetric Bohr domain with its explicit complexity cost, before the final polynomial simplification in local symmetry.

theorem TrilinearHT.Auto.graphLocalCorrelation_norm_le {q : ℕ} [NeZero q] (w : ZMod q → ℝ) (hw : ∀ (h : ZMod q), |w h| ≤ 1) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) : ‖graphLocalCorrelation w M a b c‖ ≤ 1

A graph correlation of four unit-bounded factors has modulus at most one.

noncomputable def TrilinearHT.Auto.graphSymmetryDecayConstant (C : ℝ) (d : ℕ) (s β ζ : ℝ) : ℝ

The coefficient in the local alternating Fourier decay estimate.

Equations

• TrilinearHT.Auto.graphSymmetryDecayConstant C d s β ζ = C * ↑d / (s * β * (ζ ^ 4 / 8))

theorem TrilinearHT.Auto.graph_local_symmetry_at_radius {q : ℕ} [NeZero q] (hq : Odd q) (cutoff : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S : Finset (ZMod q)) {r s ρ ζ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hs : 0 < s) (hsr : s ≤ r) (hρ : r + 2 * s ≤ ρ) (h4s : 4 * s ≤ ρ) (hζ : 0 < ζ) (htol : 2 * max (↑L) 1 * ↑S.card * s / r ≤ ζ ^ 2 / 2) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (hcorr : ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S r) M a b c‖) : ∃ (S' : Finset (ZMod q)) (t : ℝ), S ⊆ S' ∧ 0 < t ∧ t < s ∧ (∀ x ∈ graphBohrSet S' t, ∀ y ∈ graphBohrSet S' t, ‖graphAlternatingPhase M x y‖ ≤ ζ / 1000) ∧ ↑S'.card + Real.log (1 / t) ≤ 2 * ↑S.card + 10 ^ 20 * (1 + Real.log (1 / (graphBohrMass cutoff S s * (ζ ^ 4 / 8)))) ^ 4 + Real.log (1 / s) + Real.log (1 / ζ) + Real.log 1000000 + Real.log (graphSymmetryDecayConstant (max (↑L) 1) S.card s (graphBohrMass cutoff S s) ζ + 1)

Assemble local symmetry at any inner radius satisfying the source's domain and translation tolerances, retaining an explicit complexity cost for the final budget.

noncomputable def TrilinearHT.Auto.graphSymmetryBudget (d : ℕ) (r ζ : ℝ) : ℝ

The source polynomial budget for local symmetry.

Equations

• TrilinearHT.Auto.graphSymmetryBudget d r ζ = ↑d + Real.log (1 / r) + Real.log (1 / ζ) + 1

theorem TrilinearHT.Auto.graphSymmetryBudget_bounds (d : ℕ) {r ζ : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) : 1 ≤ graphSymmetryBudget d r ζ ∧ ↑d ≤ graphSymmetryBudget d r ζ ∧ Real.log (1 / r) ≤ graphSymmetryBudget d r ζ ∧ Real.log (1 / ζ) ≤ graphSymmetryBudget d r ζ

theorem TrilinearHT.Auto.localSymmetryInnerRadius_log (d : ℕ) {C r ζ : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) : Real.log (1 / localSymmetryInnerRadius C d r ζ) = Real.log (1 / r) + 2 * Real.log (1 / ζ) + Real.log 1000 + Real.log (C + 1) + Real.log (↑d + 1)

Exact logarithmic expansion of the inner radius when the correlation is at most one.

theorem TrilinearHT.Auto.localSymmetryInnerRadius_log_bound (d : ℕ) {C r ζ : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) : Real.log (1 / localSymmetryInnerRadius C d r ζ) ≤ (C + 1010) * graphSymmetryBudget d r ζ

The logarithmic inner-radius loss is linear in the source budget.

theorem TrilinearHT.Auto.graph_mass_log_bound (d : ℕ) {s β : ℝ} (hs : 0 < s) (hbound : (s / 6) ^ d ≤ β) : Real.log (1 / β) ≤ ↑d * Real.log (6 / s)

A polynomial Bohr mass lower bound becomes the exact logarithmic mass estimate.

theorem TrilinearHT.Auto.graph_symmetry_threshold_log {ζ : ℝ} (hζ : 0 < ζ) : Real.log (1 / (ζ ^ 4 / 8)) = 4 * Real.log (1 / ζ) + Real.log 8

Exact logarithmic cost of the fourth-power spectrum threshold.

theorem TrilinearHT.Auto.graphSymmetryDecayConstant_log (d : ℕ) {C s β ζ : ℝ} (hC : 0 ≤ C) (hs : 0 < s) (hs1 : s ≤ 1) (hβ : 0 < β) (hβ1 : β ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) : Real.log (graphSymmetryDecayConstant C d s β ζ + 1) ≤ Real.log (C + 1) + Real.log (↑d + 1) + Real.log (1 / s) + Real.log (1 / β) + 4 * Real.log (1 / ζ) + Real.log 8

The logarithm of the decay constant loses only logarithms of the mass and radius.

theorem TrilinearHT.Auto.graph_symmetry_parameter_bounds (d : ℕ) {C r ζ β : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hβ : 0 < β) (hβ1 : β ≤ 1) (hβlower : (localSymmetryInnerRadius C d r ζ / 6) ^ d ≤ β) : have s := localSymmetryInnerRadius C d r ζ; have K := C + 10000; have P := graphSymmetryBudget d r ζ; Real.log (1 / s) ≤ K * P ∧ Real.log (1 / β) ≤ 2 * K * P ^ 2 ∧ 1 + Real.log (1 / (β * (ζ ^ 4 / 8))) ≤ 4 * K * P ^ 2 ∧ Real.log (graphSymmetryDecayConstant C d s β ζ + 1) ≤ 6 * K * P ^ 2

All logarithmic parameters in local symmetry have polynomial source-budget bounds; blueprint lem:local-symmetry, lines 1015-1016.

theorem TrilinearHT.Auto.graph_symmetry_complexity_bound (d : ℕ) {C r ζ β : ℝ} (hC : 0 ≤ C) (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hβ : 0 < β) (hβ1 : β ≤ 1) (hβlower : (localSymmetryInnerRadius C d r ζ / 6) ^ d ≤ β) : 2 * ↑d + 10 ^ 20 * (1 + Real.log (1 / (β * (ζ ^ 4 / 8)))) ^ 4 + Real.log (1 / localSymmetryInnerRadius C d r ζ) + Real.log (1 / ζ) + Real.log 1000000 + Real.log (graphSymmetryDecayConstant C d (localSymmetryInnerRadius C d r ζ) β ζ + 1) ≤ 10 ^ 30 * (C + 10000) ^ 4 * graphSymmetryBudget d r ζ ^ 8

The explicit local-symmetry construction has degree-eight polynomial complexity.

theorem TrilinearHT.Auto.graph_local_symmetry {q : ℕ} [NeZero q] (hq : Odd q) (cutoff : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S : Finset (ZMod q)) {r ρ ζ : ℝ} (hr : 0 < r) (hrρ : r ≤ ρ / 100) (hρ1 : ρ < 1) (hζ : 0 < ζ) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (hcorr : ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S r) M a b c‖) : ∃ (S' : Finset (ZMod q)) (t : ℝ), S ⊆ S' ∧ 0 < t ∧ t < r ∧ (∀ x ∈ graphBohrSet S' t, ∀ y ∈ graphBohrSet S' t, ‖graphAlternatingPhase M x y‖ ≤ ζ / 1000) ∧ ↑S'.card + Real.log (1 / t) ≤ 10 ^ 30 * (max (↑L) 1 + 10000) ^ 4 * graphSymmetryBudget S.card r ζ ^ 8

Quantitative local symmetry, with an explicit uniform degree-eight bound. This is blueprint lem:local-symmetry, including its original correlation hypothesis.

theorem TrilinearHT.Auto.local_symmetry (cutoff : ℝ → ℝ) (hcont : ContDiff ℝ 1 cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) : ∃ (C : ℝ), 0 < C ∧ ∀ (q : ℕ) [inst : NeZero q], Odd q → ∀ (S : Finset (ZMod q)) (r ρ ζ : ℝ), 0 < r → r ≤ ρ / 100 → ρ < 1 → 0 < ζ → ∀ (M : ZMod q → ZMod q), (∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) → ∀ (a b c : ZMod q → ℂ), (∀ (x : ZMod q), ‖a x‖ ≤ 1) → (∀ (x : ZMod q), ‖b x‖ ≤ 1) → (∀ (x : ZMod q), ‖c x‖ ≤ 1) → ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S r) M a b c‖ → ∃ (S' : Finset (ZMod q)) (t : ℝ), S ⊆ S' ∧ 0 < t ∧ t < r ∧ (∀ x ∈ graphBohrSet S' t, ∀ y ∈ graphBohrSet S' t, ‖graphAlternatingPhase M x y‖ ≤ ζ / 1000) ∧ ↑S'.card + Real.log (1 / t) ≤ C * graphSymmetryBudget S.card r ζ ^ 8

Blueprint lem:local-symmetry: a fixed smooth cutoff admits a uniform polynomial local-symmetry theorem. The exponent eight and the constant are independent of the modulus, frequencies, radius and correlation. Only additivity in the stated Bohr domain is used.

theorem TrilinearHT.Auto.locally_additive_zsmul {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] (U : Set G) (M : G → H) (hM0 : M 0 = 0) (hadd : ∀ x ∈ U, ∀ y ∈ U, x + y ∈ U → M (x + y) = M x + M y) (v : G) {A : ℤ} (hA : 1 ≤ A) (hpath : ∀ (k : ℤ), |k| ≤ A → k • v ∈ U) (z : ℤ) (hz : |z| ≤ A) : M (z • v) = z • M v

Local additivity along a bounded positive and negative integer path gives the expected scalar identity without assuming global additivity.

theorem TrilinearHT.Auto.locally_additive_integer_box {ι : Type u_1} {G : Type u_2} {H : Type u_3} [Fintype ι] [AddCommGroup G] [AddCommGroup H] (U : Set G) (M : G → H) (hadd : ∀ x ∈ U, ∀ y ∈ U, x + y ∈ U → M (x + y) = M x + M y) (v : ι → G) (A : ι → ℤ) (hA : ∀ (i : ι), 0 ≤ A i) (hbox : ∀ (z : ι → ℤ), (∀ (i : ι), |z i| ≤ A i) → ∑ i : ι, z i • v i ∈ U) (z : ι → ℤ) (hz : ∀ (i : ι), |z i| ≤ A i) : M (∑ i : ι, z i • v i) = ∑ i : ι, z i • M (v i)

A locally additive map agrees with its linear coordinate formula throughout an integer box contained in its domain; blueprint lem:local-chart, lines 1043-1047.

theorem TrilinearHT.Auto.cyclic_linear_quadratic_phase {ι : Type u_1} [Fintype ι] {q : ℕ} [NeZero q] (m v : ι → ZMod q) (z : ι → ℤ) : ZMod.toAddCircle ((∑ i : ι, z i • m i) * ∑ i : ι, z i • v i) = ↑(((∑ i : ι, ↑(z i) * ↑(m i).val) * ∑ i : ι, ↑(z i) * ↑(v i).val) / ↑q)

The product of two integer linear forms in a cyclic group is the reduction modulo one of the corresponding ordinary real quadratic polynomial.

theorem TrilinearHT.Auto.finite_weighted_set_average {G : Type u_1} [Fintype G] [AddCommGroup G] (H : Finset G) (w : G → ℝ) : (Finset.univ.expect fun (x : G) => Finset.univ.expect fun (h : G) => w h * (↑H).indicator 1 (x + h)) = ↑H.dens * Finset.univ.expect fun (h : G) => w h

theorem TrilinearHT.Auto.finite_weighted_set_translate {G : Type u_1} [Fintype G] [AddCommGroup G] (H : Finset G) (w : G → ℝ) (hpos : 0 < ↑H.dens * Finset.univ.expect fun (h : G) => w h) : ∃ (x : G) (h₀ : G), ((↑H.dens * Finset.univ.expect fun (h : G) => w h) ≤ Finset.univ.expect fun (h : G) => w h * (↑H).indicator 1 (x + h)) ∧ 0 < w h₀ ∧ x + h₀ ∈ H

theorem TrilinearHT.Auto.graph_frequency_affine_on_translate {q : ℕ} [NeZero q] (H S : Finset (ZMod q)) (ξ M : ZMod q → ZMod q) {r ρ : ℝ} (hr : 0 ≤ r) (hρ : 2 * r ≤ ρ) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ v ∈ graphBohrSet S ρ, u + v ∈ graphBohrSet S ρ → M (u + v) = M u + M v) (hdiff : ∀ u ∈ H, ∀ v ∈ H, u - v ∈ graphBohrSet S ρ → ξ u - ξ v = 2 * M (u - v)) {x h₀ h : ZMod q} (h₀H : x + h₀ ∈ H) (hhH : x + h ∈ H) (h₀B : h₀ ∈ graphBohrSet S r) (hhB : h ∈ graphBohrSet S r) : ξ (x + h) = ξ (x + h₀) - 2 * M h₀ + 2 * M h

theorem TrilinearHT.Auto.complex_phase_alignment (z : ℂ) : ∃ (c : ℂ), ‖c‖ = 1 ∧ c * z = ↑‖z‖

theorem TrilinearHT.Auto.finite_supported_phase_alignment {G : Type u_1} (P : G → Prop) [DecidablePred P] (z : G → ℂ) : ∃ (c : G → ℂ), (∀ (h : G), ‖c h‖ ≤ 1) ∧ (∀ (h : G), P h → ‖c h‖ = 1) ∧ (∀ (h : G), ¬P h → c h = 0) ∧ ∀ (h : G), c h * z h = if P h then ↑‖z h‖ else 0

theorem TrilinearHT.Auto.finite_weighted_phase_lower_bound {G : Type u_1} [Fintype G] (P : G → Prop) [DecidablePred P] (w : G → ℝ) (z c : G → ℂ) (hw : ∀ (h : G), 0 ≤ w h) (hc : ∀ (h : G), c h * z h = if P h then ↑‖z h‖ else 0) {a : ℝ} (hz : ∀ (h : G), P h → a ≤ ‖z h‖) : (a * Finset.univ.expect fun (h : G) => w h * if P h then 1 else 0) ≤ ‖Finset.univ.expect fun (h : G) => ↑(w h) * (c h * z h)‖

theorem TrilinearHT.Auto.graph_initial_phase_correlation {q : ℕ} [NeZero q] (P : ZMod q → Prop) [DecidablePred P] (w : ZMod q → ℝ) (hw : ∀ (h : ZMod q), 0 ≤ w h) (f : ZMod q → ℂ) (M : ZMod q → ZMod q) (x₀ ξ₀ : ZMod q) {a : ℝ} (hcor : ∀ (h : ZMod q), P h → a ≤ ‖Finset.univ.expect fun (x : ZMod q) => f (x + h + x₀) * (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-((ξ₀ + 2 * M h) * x))‖) : ∃ (c : ZMod q → ℂ), (∀ (h : ZMod q), ‖c h‖ ≤ 1) ∧ (∀ (h : ZMod q), ¬P h → c h = 0) ∧ (a * Finset.univ.expect fun (h : ZMod q) => w h * if P h then 1 else 0) ≤ ‖graphLocalCorrelation w M (fun (x : ZMod q) => f (x + x₀)) (fun (x : ZMod q) => (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-(ξ₀ * x))) c‖

theorem TrilinearHT.Auto.graph_initial_correlation_from_derivatives {q : ℕ} [NeZero q] (H S : Finset (ZMod q)) (ξ M : ZMod q → ZMod q) (w : ZMod q → ℝ) (f : ZMod q → ℂ) {r ρ a : ℝ} (hr : 0 ≤ r) (hρ : 2 * r ≤ ρ) (ha : 0 ≤ a) (hw : ∀ (h : ZMod q), 0 ≤ w h) (hsupp : ∀ (h : ZMod q), w h ≠ 0 → h ∈ graphBohrSet S r) (hpos : 0 < ↑H.dens * Finset.univ.expect fun (h : ZMod q) => w h) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ v ∈ graphBohrSet S ρ, u + v ∈ graphBohrSet S ρ → M (u + v) = M u + M v) (hdiff : ∀ u ∈ H, ∀ v ∈ H, u - v ∈ graphBohrSet S ρ → ξ u - ξ v = 2 * M (u - v)) (hcor : ∀ h ∈ H, a ≤ ‖Finset.univ.expect fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-(ξ h * x))‖) : ∃ (x₀ : ZMod q) (ξ₀ : ZMod q) (c : ZMod q → ℂ), (∀ (h : ZMod q), ‖c h‖ ≤ 1) ∧ a * (↑H.dens * Finset.univ.expect fun (h : ZMod q) => w h) ≤ ‖graphLocalCorrelation w M (fun (x : ZMod q) => f (x + x₀)) (fun (x : ZMod q) => (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-(ξ₀ * x))) c‖

theorem TrilinearHT.Auto.graph_initial_correlation_log (d N : ℕ) {δ ρ α β K : ℝ} (hδ : 0 < δ) (hρ : 0 < ρ) (hK : 0 < K) (hα : δ ^ N / K ≤ α) (hβ : (ρ / 600) ^ d ≤ β) : Real.log (1 / (δ ^ 4 * α * β / √2)) ≤ (↑N + 4) * Real.log (1 / δ) + Real.log K + Real.log √2 + ↑d * (Real.log 600 + Real.log (1 / ρ))

theorem TrilinearHT.Auto.graph_initial_correlation_log_budget (d N : ℕ) {δ ρ α β K A B : ℝ} (hδ : 0 < δ) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hK : 0 < K) (hα : δ ^ N / K ≤ α) (hβ : (ρ / 600) ^ d ≤ β) (hA : 1 ≤ A) (hB : 1 ≤ B) (hδB : Real.log (1 / δ) ≤ B) (hd : ↑d + Real.log (1 / ρ) ≤ A * B ^ 4) : Real.log (1 / (δ ^ 4 * α * β / √2)) ≤ (↑N + 4 + K + 2 + 600 * A + A ^ 2) * B ^ 8

theorem TrilinearHT.Auto.finite_weighted_shift_error {G : Type u_1} [Fintype G] [AddCommGroup G] (w μ : G → ℝ) (hμ : ∀ (t : G), 0 ≤ μ t) (hμmass : (Finset.univ.expect fun (t : G) => μ t) = 1) (F : G → ℂ) (hF : ∀ (h : G), ‖F h‖ ≤ 1) {ε : ℝ} (htrans : ∀ (h t : G), μ t ≠ 0 → |w (h + t) - w h| ≤ ε) : ‖(Finset.univ.expect fun (h : G) => ↑(w h) * F h) - Finset.univ.expect fun (h : G) => ↑(w h) * Finset.univ.expect fun (t : G) => ↑(μ t) * F (h + t)‖ ≤ ε

theorem TrilinearHT.Auto.finite_weighted_shift_select {G : Type u_1} [Fintype G] [AddCommGroup G] (w μ : G → ℝ) (hw : ∀ (h : G), 0 ≤ w h) (hwmass : (Finset.univ.expect fun (h : G) => w h) ≤ 1) (hμ : ∀ (t : G), 0 ≤ μ t) (hμmass : (Finset.univ.expect fun (t : G) => μ t) = 1) (F : G → ℂ) (hF : ∀ (h : G), ‖F h‖ ≤ 1) {ζ ε : ℝ} (hζ : ε < ζ) (hcorr : ζ ≤ ‖Finset.univ.expect fun (h : G) => ↑(w h) * F h‖) (htrans : ∀ (h t : G), μ t ≠ 0 → |w (h + t) - w h| ≤ ε) : ∃ (h : G), w h ≠ 0 ∧ ζ - ε ≤ ‖Finset.univ.expect fun (t : G) => ↑(μ t) * F (h + t)‖

theorem TrilinearHT.Auto.graph_local_shift_select {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hw : ∀ (h : ZMod q), 0 ≤ w h) (hwmass : (Finset.univ.expect fun (h : ZMod q) => w h) ≤ 1) (hμ : ∀ (t : ZMod q), 0 ≤ μ t) (hμmass : (Finset.univ.expect fun (t : ZMod q) => μ t) = 1) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) {ζ ε : ℝ} (hζ : ε < ζ) (hcorr : ζ ≤ ‖graphLocalCorrelation w M a b c‖) (htrans : ∀ (h t : ZMod q), μ t ≠ 0 → |w (h + t) - w h| ≤ ε) (hadd : ∀ (h : ZMod q), w h ≠ 0 → ∀ (t : ZMod q), μ t ≠ 0 → M (h + t) = M h + M t) : ∃ (h : ZMod q), w h ≠ 0 ∧ ζ - ε ≤ ‖graphLocalCorrelation μ M (fun (x : ZMod q) => a (x + h)) (fun (x : ZMod q) => b x * ZMod.stdAddChar (-(2 * M h * x))) fun (t : ZMod q) => c (h + t)‖

theorem TrilinearHT.Auto.graph_bohr_shift_select {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S T : Finset (ZMod q)) (hST : S ⊆ T) {r s ρ ζ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hs : 0 < s) (hsr : s ≤ r) (hrρ : r + s ≤ ρ) (hζ : 0 < ζ) (herror : max (↑L) 1 * ↑S.card * s / r ≤ ζ / 100) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (hcorr : ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S r) M a b c‖) : ∃ h ∈ graphBohrSet S r, ζ / 2 ≤ ‖graphLocalCorrelation (graphBohrMeasure cutoff T s) M (fun (x : ZMod q) => a (x + h)) (fun (x : ZMod q) => b x * ZMod.stdAddChar (-(2 * M h * x))) fun (t : ZMod q) => c (h + t)‖

theorem TrilinearHT.Auto.graph_correlation_localization_explicit {q : ℕ} [NeZero q] (w μ : ZMod q → ℝ) (hμ : (Finset.univ.expect fun (u : ZMod q) => μ u) = 1) (M : ZMod q → ZMod q) (a b c : ZMod q → ℂ) {ζ : ℝ} (hζ : ζ ≤ ‖graphLocalCorrelation w M a b c‖) : ∃ (y : ZMod q), ζ ≤ ‖graphLocalizedCorrelation w μ M (fun (x : ZMod q) => a (x + y)) (fun (x : ZMod q) => b (x + y)) fun (h : ZMod q) => c h * ZMod.stdAddChar (-(2 * M h * y))‖

theorem TrilinearHT.Auto.graph_quadratic_polarization {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (u t : ZMod q) (hM : M (u + t) = M u + M t) : ZMod.stdAddChar (-(M u * t + M t * u)) = ZMod.stdAddChar (M u * u) * ZMod.stdAddChar (M t * t) * ZMod.stdAddChar (-(M (u + t) * (u + t)))

theorem TrilinearHT.Auto.graph_skew_character_error {q : ℕ} [NeZero q] (M : ZMod q → ZMod q) (u t : ZMod q) : ‖ZMod.stdAddChar (-(2 * M t * u)) - ZMod.stdAddChar (-(M u * t + M t * u))‖ ≤ 2 * Real.pi * ‖graphAlternatingPhase M u t‖

theorem TrilinearHT.Auto.graph_localized_polarization_error {q : ℕ} [NeZero q] (μ : ZMod q → ℝ) (hμ : ∀ (x : ZMod q), 0 ≤ μ x) (hμmass : (Finset.univ.expect fun (x : ZMod q) => μ x) = 1) (M : ZMod q → ZMod q) (D : Set (ZMod q)) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) {κ : ℝ} (hskew : ∀ (u t : ZMod q), μ u ≠ 0 → μ t ≠ 0 → ‖graphAlternatingPhase M u t‖ ≤ κ) (hadd : ∀ (u t : ZMod q), μ u ≠ 0 → μ t ≠ 0 → M (u + t) = M u + M t) (hD : ∀ (u t : ZMod q), μ u ≠ 0 → μ t ≠ 0 → u + t ∈ D) : ‖graphLocalizedCorrelation μ μ M a b c - Finset.univ.expect fun (u : ZMod q) => Finset.univ.expect fun (t : ZMod q) => ↑(μ u) * b u * ZMod.stdAddChar (M u * u) * (↑(μ t) * c t * ZMod.stdAddChar (M t * t)) * D.indicator (fun (v : ZMod q) => a v * ZMod.stdAddChar (-(M v * v))) (u + t)‖ ≤ 2 * Real.pi * κ

theorem TrilinearHT.Auto.graph_bohr_polarized_correlation {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S : Finset (ZMod q)) {s ρ ζ : ℝ} (hs : 0 < s) (hs1 : s < 1 / 8) (hsρ : 2 * s ≤ ρ) (hζ : 0 < ζ) (M : ZMod q → ZMod q) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ t ∈ graphBohrSet S ρ, u + t ∈ graphBohrSet S ρ → M (u + t) = M u + M t) (hskew : ∀ u ∈ graphBohrSet S s, ∀ t ∈ graphBohrSet S s, ‖graphAlternatingPhase M u t‖ ≤ ζ / 1000) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (hcorr : ζ / 2 ≤ ‖graphLocalizedCorrelation (graphBohrMeasure cutoff S s) (graphBohrMeasure cutoff S s) M a b c‖) : have μ := graphBohrMeasure cutoff S s; ζ / 4 ≤ ‖Finset.univ.expect fun (u : ZMod q) => Finset.univ.expect fun (t : ZMod q) => ↑(μ u) * b u * ZMod.stdAddChar (M u * u) * (↑(μ t) * c t * ZMod.stdAddChar (M t * t)) * (↑(graphBohrSet S (2 * s))).indicator (fun (v : ZMod q) => a v * ZMod.stdAddChar (-(M v * v))) (u + t)‖

theorem TrilinearHT.Auto.graph_bohr_weighted_quadratic_correlation {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S : Finset (ZMod q)) {s ρ ζ : ℝ} (hs : 0 < s) (hs1 : s < 1 / 8) (hsρ : 2 * s ≤ ρ) (hζ : 0 < ζ) (M : ZMod q → ZMod q) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ t ∈ graphBohrSet S ρ, u + t ∈ graphBohrSet S ρ → M (u + t) = M u + M t) (hskew : ∀ u ∈ graphBohrSet S s, ∀ t ∈ graphBohrSet S s, ‖graphAlternatingPhase M u t‖ ≤ ζ / 1000) (a b c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hb : ∀ (x : ZMod q), ‖b x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (hcorr : ζ / 2 ≤ ‖graphLocalizedCorrelation (graphBohrMeasure cutoff S s) (graphBohrMeasure cutoff S s) M a b c‖) : have β := graphBohrMass cutoff S s; ∃ (ξ : ZMod q), ζ * β * √β / 4 ≤ ‖Finset.univ.expect fun (u : ZMod q) => ↑(graphBohrWeight cutoff S s u) * b u * ZMod.stdAddChar (M u * u - ξ * u)‖

theorem TrilinearHT.Auto.graph_quadratic_correlation_recover {q : ℕ} [NeZero q] (w : ZMod q → ℝ) (f : ZMod q → ℂ) (M : ZMod q → ZMod q) (a y ξ : ZMod q) : ‖Finset.univ.expect fun (u : ZMod q) => ↑(w u) * ((starRingEnd ℂ) (f (u + y)) * ZMod.stdAddChar (-(a * (u + y)))) * ZMod.stdAddChar (M u * u - ξ * u)‖ = ‖Finset.univ.expect fun (u : ZMod q) => ↑(w u) * f (u + y) * ZMod.stdAddChar (-(M u * u) + (a + ξ) * u)‖

theorem TrilinearHT.Auto.graph_bohr_local_quadratic_correlation {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) {L : NNReal} (hLip : LipschitzWith L cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (S T : Finset (ZMod q)) (hST : S ⊆ T) {r s ρ ζ : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 8) (hs : 0 < s) (hsr : s ≤ r) (hrρ : r + s ≤ ρ) (hζ : 0 < ζ) (herror : max (↑L) 1 * ↑S.card * s / r ≤ ζ / 100) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (hskew : ∀ u ∈ graphBohrSet T s, ∀ t ∈ graphBohrSet T s, ‖graphAlternatingPhase M u t‖ ≤ ζ / 1000) (a f c : ZMod q → ℂ) (ha : ∀ (x : ZMod q), ‖a x‖ ≤ 1) (hf : ∀ (x : ZMod q), ‖f x‖ ≤ 1) (hc : ∀ (x : ZMod q), ‖c x‖ ≤ 1) (ξ₀ : ZMod q) (hcorr : ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S r) M a (fun (x : ZMod q) => (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-(ξ₀ * x))) c‖) : have β := graphBohrMass cutoff T s; ∃ (y : ZMod q) (ℓ : ZMod q), ζ * β * √β / 4 ≤ ‖Finset.univ.expect fun (u : ZMod q) => ↑(graphBohrWeight cutoff T s u) * f (u + y) * ZMod.stdAddChar (-(M u * u) + ℓ * u)‖

theorem TrilinearHT.Auto.local_inverse_polynomial_budget (d D : ℕ) {P R Z T V B G : ℝ} (hP : 100000 ≤ P) (hT0 : 0 ≤ T) (hV0 : 0 ≤ V) (hd : ↑d + R ≤ P) (hZ : Z ≤ P) (hDT : ↑D + T ≤ P * (3 * P) ^ 8) (hV : V ≤ T + Z + 2 * R + P + 20000 * (↑D + 1) ^ 2) (hB : B ≤ ↑D * (6 + V)) (hG : G ≤ Z + 3 / 2 * B + 4) : ↑D + V + 1 ≤ P ^ 22 ∧ G ≤ P ^ 34

theorem TrilinearHT.Auto.graph_local_inverse_log_budget (d D : ℕ) {P ρ t r ζ β C K : ℝ} (hP : 100000 ≤ P) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (ht : 0 < t) (ht1 : t ≤ 1) (hr : 0 < r) (hr1 : r ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hKP : K ≤ P) (hd : ↑d + Real.log (1 / ρ) ≤ P) (hZ : Real.log (1 / ζ) ≤ P) (hC : Real.log C ≤ P) (hDT : ↑D + Real.log (1 / t) ≤ K * graphSymmetryBudget d (ρ / 100) ζ ^ 8) (hV : Real.log (1 / r) ≤ Real.log (1 / t) + Real.log (1 / ζ) + 2 * Real.log (1 / ρ) + Real.log C + 20000 * (↑D + 1) ^ 2) (hβ : (r / 6) ^ D ≤ β) : ↑D + Real.log (1 / r) + 1 ≤ P ^ 22 ∧ Real.log (1 / (ζ * β * √β / 4)) ≤ P ^ 34

Cyclic rational lattices

noncomputable def TrilinearHT.Auto.cyclicCoordinateEquiv {ι : Type u_1} [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ

A triangular coordinate change whose distinguished basis vector has denominator q. It provides the full lattice used in blueprint lem:local-chart, lines 1035-1039.

Equations

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

noncomputable def TrilinearHT.Auto.cyclicLiftBasis {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) : Module.Basis ι ℝ (EuclideanSpace ℝ ι)

A Euclidean full basis for the cyclic lift lattice.

Equations

• TrilinearHT.Auto.cyclicLiftBasis q a i₀ = (Pi.basisFun ℝ ι).map (TrilinearHT.Auto.cyclicCoordinateEquiv q a i₀ ≪≫ₗ (WithLp.linearEquiv 2 ℝ (ι → ℝ)).symm)

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.cyclicLiftLattice {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) : Submodule ℤ (EuclideanSpace ℝ ι)

The integer span of the rational cyclic basis, automatically a full discrete lattice.

Equations

• TrilinearHT.Auto.cyclicLiftLattice q a i₀ = Submodule.span ℤ (Set.range ⇑(TrilinearHT.Auto.cyclicLiftBasis q a i₀))

theorem TrilinearHT.Auto.cyclicLiftBasis_repr {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (x : EuclideanSpace ℝ ι) (i : ι) : ((cyclicLiftBasis q a i₀).repr x) i = if i = i₀ then ↑q * x.ofLp i₀ else x.ofLp i - ↑(a i) * x.ofLp i₀

Real coordinates in the cyclic basis have a triangular explicit formula.

theorem TrilinearHT.Auto.cyclicLiftLattice_integer_coordinates {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (x : ↥(cyclicLiftLattice q a i₀)) (i : ι) : ↑(((Module.Basis.restrictScalars ℤ (cyclicLiftBasis q a i₀)).repr x) i) = if i = i₀ then ↑q * (↑x).ofLp i₀ else (↑x).ofLp i - ↑(a i) * (↑x).ofLp i₀

The integer coordinates of a lattice point agree with its real basis coordinates.

theorem TrilinearHT.Auto.integerVector_mem_cyclicLiftLattice {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (z : ι → ℤ) : (WithLp.toLp 2 fun (i : ι) => ↑(z i)) ∈ cyclicLiftLattice q a i₀

Every integer vector belongs to the cyclic lift lattice.

noncomputable def TrilinearHT.Auto.cyclicLiftProjection {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) : ↥(cyclicLiftLattice q a i₀) →+ ZMod q

The cyclic quotient is the distinguished integer basis coefficient modulo q.

Equations

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

theorem TrilinearHT.Auto.cyclicLiftProjection_basis {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ i : ι) : (cyclicLiftProjection q a i₀) ((Module.Basis.restrictScalars ℤ (cyclicLiftBasis q a i₀)) i) = if i = i₀ then 1 else 0

theorem TrilinearHT.Auto.cyclicLiftProjection_eq_zero_iff {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (x : ↥(cyclicLiftLattice q a i₀)) : (cyclicLiftProjection q a i₀) x = 0 ↔ ∀ (i : ι), ∃ (z : ℤ), (↑x).ofLp i = ↑z

The kernel consists exactly of the vectors with integer coordinates.

def TrilinearHT.Auto.cyclicLiftFrequency {ι : Type u_1} [DecidableEq ι] (q : ℕ) (a : ι → ℤ) (i₀ i : ι) : ZMod q

The frequency associated to each cyclic lift coordinate, with distinguished frequency one.

Equations

• TrilinearHT.Auto.cyclicLiftFrequency q a i₀ i = if i = i₀ then 1 else ↑(a i)

theorem TrilinearHT.Auto.cyclicLiftProjection_character {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (x : ↥(cyclicLiftLattice q a i₀)) (i : ι) : ↑((↑x).ofLp i) = ZMod.toAddCircle (cyclicLiftFrequency q a i₀ i * (cyclicLiftProjection q a i₀) x)

Reduction modulo the integer lattice recovers every specified cyclic character.

theorem TrilinearHT.Auto.cyclicLiftProjection_injective_near {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℕ) [NeZero q] (a : ι → ℤ) (i₀ : ι) (x y : ↥(cyclicLiftLattice q a i₀)) (hsmall : ‖↑x - ↑y‖ < 1) (heq : (cyclicLiftProjection q a i₀) x = (cyclicLiftProjection q a i₀) y) : x = y

Two cyclic lifts less than one apart cannot have the same projection unless equal.

theorem TrilinearHT.Auto.integer_lattice_dual_coordinates {ι : Type u_1} [Fintype ι] {n : ℕ} (L : Submodule ℤ (EuclideanSpace ℝ ι)) (hZ : ∀ (z : ι → ℤ), (WithLp.toLp 2 fun (j : ι) => ↑(z j)) ∈ L) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ι)) (hb : Submodule.span ℤ (Set.range ⇑b) = L) (θ : EuclideanSpace ℝ ι) (hθ : θ ∈ L) : ∃ (U : Fin n → ι → ℤ) (t : Fin n → ℤ), (∀ (i : Fin n) (j : ι), ((euclideanDualBasis b) i).ofLp j = ↑(U i j)) ∧ (∀ (i : Fin n), inner ℝ ((euclideanDualBasis b) i) θ = ↑(t i)) ∧ (∀ (x : EuclideanSpace ℝ ι) (i : Fin n), (b.repr x) i = ∑ j : ι, ↑(U i j) * x.ofLp j) ∧ ∀ (m : ℤ) (k : ι → ℤ) (i : Fin n), (b.repr (m • θ - WithLp.toLp 2 fun (j : ι) => ↑(k j))) i = ↑(t i * m - ∑ j : ι, U i j * k j)

A full lattice containing the integer lattice has integral dual coordinates. For a lattice vector θ, its basis-coordinate forms on n θ - k have integer coefficients; blueprint lem:local-chart, lines 1054-1057.

theorem TrilinearHT.Auto.latticeBoxRadius_pos {n : ℕ} (hn : 0 < n) : 0 < latticeBoxRadius n

def TrilinearHT.Auto.chartCouplingMatrix (d : ℕ) : Matrix (Fin (d + d)) (Fin (d + d)) ℚ

The integral lower-left identity block used to encode a horizontal linear phase.

Equations

• TrilinearHT.Auto.chartCouplingMatrix d i j = Fin.addCases (fun (x : Fin d) => 0) (fun (a : Fin d) => Fin.addCases (fun (b : Fin d) => if a = b then 1 else 0) (fun (x : Fin d) => 0) j) i

theorem TrilinearHT.Auto.chartCouplingMatrix_height (d : ℕ) (i j : Fin (d + d)) : chartRationalHeight (chartCouplingMatrix d i j) = 1

theorem TrilinearHT.Auto.chartMatrixPhase_coupling {d : ℕ} (z w : Fin (d + d) → ℝ) : chartMatrixPhase (chartCouplingMatrix d) z w = ∑ i : Fin d, z (Fin.natAdd d i) * w (Fin.castAdd d i)

noncomputable def TrilinearHT.Auto.coupledQuadraticChart {d : ℕ} (A B : QuadraticChartData d) : QuadraticChartData (d + d)

Couple the two coordinate blocks through the lower-left identity matrix. The amplitudes and ordinary phases are those of the product chart.

Equations

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

theorem TrilinearHT.Auto.coupledQuadraticChart_summand {d : ℕ} (A B : QuadraticChartData d) (y : ℝ) (n m : Fin d → ℤ) : quadraticChartLatticeSummand (coupledQuadraticChart A B) y (Fin.append n m) = A.amplitude (chartLatticeRemainder A y n) * ↑(Real.fourierChar (y * ∑ i : Fin d, B.horizontal i * chartLatticeRemainder A y n i)) * B.amplitude (chartLatticeRemainder B y m)

theorem TrilinearHT.Auto.chartAmplitude_finite_support {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : Function.HasFiniteSupport fun (n : Fin d → ℤ) => A.amplitude (chartLatticeRemainder A y n)

theorem TrilinearHT.Auto.coupledQuadraticChart_atom {d : ℕ} (A B : QuadraticChartData d) (y : ℝ) : quadraticChartAtom (coupledQuadraticChart A B) y = (↑(Real.fourierChar ((A.quadratic + B.quadratic) * y ^ 2 + (A.linear + B.linear) * y)) * ∑' (n : Fin d → ℤ), A.amplitude (chartLatticeRemainder A y n) * ↑(Real.fourierChar (y * ∑ i : Fin d, B.horizontal i * chartLatticeRemainder A y n i))) * ∑' (m : Fin d → ℤ), B.amplitude (chartLatticeRemainder B y m)

The coupled chart factors into a phased sum in the first lattice block and an ordinary periodization in the second block.

theorem TrilinearHT.Auto.coupledQuadraticChart_atom_of_partition {d : ℕ} (A B : QuadraticChartData d) (hB : ∀ (z : Fin d → ℝ), (∑' (m : Fin d → ℤ), B.amplitude fun (i : Fin d) => z i - ↑(m i)) = 1) (y : ℝ) : quadraticChartAtom (coupledQuadraticChart A B) y = ↑(Real.fourierChar ((A.quadratic + B.quadratic) * y ^ 2 + (A.linear + B.linear) * y)) * ∑' (n : Fin d → ℤ), A.amplitude (chartLatticeRemainder A y n) * ↑(Real.fourierChar (y * ∑ i : Fin d, B.horizontal i * chartLatticeRemainder A y n i))

A partition of unity in the second block removes that lattice sum exactly.

theorem TrilinearHT.Auto.finite_support_tsum_product {ι : Type u_1} {κ : Type u_2} [Fintype ι] (f : ι → κ → ℂ) (hf : ∀ (i : ι), Function.HasFiniteSupport (f i)) : ∑' (k : ι → κ), ∏ i : ι, f i (k i) = ∏ i : ι, ∑' (j : κ), f i j

A finite product of finitely supported series factors without convergence qualifications.

noncomputable def TrilinearHT.Auto.chartCoordinateProduct {d : ℕ} (f : ℝ → ℝ) (z : Fin d → ℝ) : ℂ

Tensor product of a real cutoff, viewed as a complex amplitude.

Equations

• TrilinearHT.Auto.chartCoordinateProduct f z = ∏ i : Fin d, ↑(f (z i))

theorem TrilinearHT.Auto.chartCoordinateProduct_smooth {d : ℕ} {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (chartCoordinateProduct f)

theorem TrilinearHT.Auto.chartCoordinateProduct_compact {d : ℕ} {f : ℝ → ℝ} (hf : HasCompactSupport f) : HasCompactSupport (chartCoordinateProduct f)

noncomputable def TrilinearHT.Auto.chartQuadraticAmplitude {d : ℕ} (f : ℝ → ℝ) (C : Fin d → Fin d → ℝ) (z : Fin d → ℝ) : ℂ

A compact product cutoff multiplied by a real quadratic phase.

Equations

• TrilinearHT.Auto.chartQuadraticAmplitude f C z = TrilinearHT.Auto.chartCoordinateProduct f z * ↑(Real.fourierChar (∑ i : Fin d, ∑ j : Fin d, C i j * z i * z j))

theorem TrilinearHT.Auto.chartQuadraticAmplitude_smooth {d : ℕ} {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (C : Fin d → Fin d → ℝ) : ContDiff ℝ (↑⊤) (chartQuadraticAmplitude f C)

theorem TrilinearHT.Auto.chartQuadraticAmplitude_compact {d : ℕ} {f : ℝ → ℝ} (hf : HasCompactSupport f) (C : Fin d → Fin d → ℝ) : HasCompactSupport (chartQuadraticAmplitude f C)

noncomputable def TrilinearHT.Auto.amplitudeQuadraticChart {d : ℕ} (θ : Fin d → ℝ) (ell : ℝ) (f : (Fin d → ℝ) → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : QuadraticChartData d

A zero-matrix chart encoding the periodization of an arbitrary smooth compact amplitude.

Equations

• TrilinearHT.Auto.amplitudeQuadraticChart θ ell f hf hc = { horizontal := θ, quadratic := ell, linear := 0, matrix := 0, amplitude := f, smooth := hf, compact := hc }

noncomputable def TrilinearHT.Auto.localizedQuadraticChart {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) : QuadraticChartData (d + d)

The source doubled-horizontal chart, with a quadratic cutoff in the first block and a tensor partition in the second; blueprint lem:local-chart, lines 1069-1076.

Equations

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

theorem TrilinearHT.Auto.compact_real_translate_finite_support (g : ℝ → ℝ) (hg : HasCompactSupport g) (x : ℝ) : Function.HasFiniteSupport fun (k : ℤ) => ↑(g (x - ↑k))

theorem TrilinearHT.Auto.chartCoordinateProduct_periodization {d : ℕ} (g : ℝ → ℝ) (hg : HasCompactSupport g) (hpart : ∀ (x : ℝ), ∑' (k : ℤ), g (x - ↑k) = 1) (z : Fin d → ℝ) : (∑' (k : Fin d → ℤ), chartCoordinateProduct g fun (i : Fin d) => z i - ↑(k i)) = 1

Tensoring a compact one-dimensional partition gives an exact lattice partition.

theorem TrilinearHT.Auto.localizedQuadraticChart_atom {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (hpart : ∀ (x : ℝ), ∑' (k : ℤ), g (x - ↑k) = 1) (y : ℝ) : quadraticChartAtom (localizedQuadraticChart θ v ell C f g hf hg hfc hgc) y = ↑(Real.fourierChar (ell * y ^ 2)) * ∑' (k : Fin d → ℤ), (chartCoordinateProduct f fun (i : Fin d) => θ i * y - ↑(k i)) * ↑(Real.fourierChar (∑ i : Fin d, ∑ j : Fin d, C i j * (θ i * y - ↑(k i)) * (θ j * y - ↑(k j)) + y * ∑ i : Fin d, v i * (θ i * y - ↑(k i))))

The local chart's actual lattice formula after canceling its tensor partition.

theorem TrilinearHT.Auto.localizedQuadraticChart_height {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (i j : Fin (d + d)) : chartRationalHeight ((localizedQuadraticChart θ v ell C f g hf hg hfc hgc).matrix i j) = 1

theorem TrilinearHT.Auto.scaled_unit_cutoff_compact (f : ℝ → ℝ) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → f x = 0) {r : ℝ} (hr : 0 < r) : HasCompactSupport fun (x : ℝ) => f (x / r)

Scaling a cutoff supported in the unit interval gives a compactly supported cutoff.

theorem TrilinearHT.Auto.integer_translate_unique {d : ℕ} (z : Fin d → ℝ) (k l : Fin d → ℤ) (hk : ∀ (i : Fin d), |z i - ↑(k i)| ≤ 1 / 2) (hl : ∀ (i : Fin d), |z i - ↑(l i)| < 1 / 2) : k = l

A centered lattice representative and a strictly shorter representative must coincide.

theorem TrilinearHT.Auto.chartCoordinateProduct_coord_lt {d : ℕ} {f : ℝ → ℝ} {r : ℝ} (hsupp : ∀ (x : ℝ), r ≤ |x| → f x = 0) (z : Fin d → ℝ) (hz : chartCoordinateProduct f z ≠ 0) (i : Fin d) : |z i| < r

theorem TrilinearHT.Auto.localizedQuadraticChart_at_center {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (hpart : ∀ (x : ℝ), ∑' (k : ℤ), g (x - ↑k) = 1) {r : ℝ} (hr : r < 1 / 2) (hsupp : ∀ (x : ℝ), r ≤ |x| → f x = 0) (y : ℝ) (k : Fin d → ℤ) (hk : ∀ (i : Fin d), |θ i * y - ↑(k i)| ≤ 1 / 2) : quadraticChartAtom (localizedQuadraticChart θ v ell C f g hf hg hfc hgc) y = (↑(Real.fourierChar (ell * y ^ 2)) * chartCoordinateProduct f fun (i : Fin d) => θ i * y - ↑(k i)) * ↑(Real.fourierChar (∑ i : Fin d, ∑ j : Fin d, C i j * (θ i * y - ↑(k i)) * (θ j * y - ↑(k j)) + y * ∑ i : Fin d, v i * (θ i * y - ↑(k i))))

The entire lattice sum is its centered term, including when that term vanishes.

theorem TrilinearHT.Auto.chartCoordinateProduct_norm_le_one {d : ℕ} (f : ℝ → ℝ) (hf : ∀ (x : ℝ), |f x| ≤ 1) (z : Fin d → ℝ) : ‖chartCoordinateProduct f z‖ ≤ 1

theorem TrilinearHT.Auto.localizedQuadraticChart_bounded {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (hpart : ∀ (x : ℝ), ∑' (k : ℤ), g (x - ↑k) = 1) {r : ℝ} (hr : r < 1 / 2) (hsupp : ∀ (x : ℝ), r ≤ |x| → f x = 0) (hunit : ∀ (x : ℝ), |f x| ≤ 1) : IsBoundedQuadraticChart (localizedQuadraticChart θ v ell C f g hf hg hfc hgc)

Compact unit cutoffs of width less than one yield a chart bounded on the entire real line.

theorem TrilinearHT.Auto.derivative_product_geometric {E : Type u_1} {A : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedCommRing A] [NormedAlgebra ℝ A] {f g : E → A} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : E) {m : ℕ} {R T : ℝ} (hR : 0 ≤ R) (_hT : 0 ≤ T) (hfi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f x‖ ≤ R ^ i) (hgi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g x‖ ≤ T ^ i) : ‖iteratedFDeriv ℝ m (fun (y : E) => f y * g y) x‖ ≤ (R + T) ^ m

Geometric derivative bounds combine by adding their bases.

theorem TrilinearHT.Auto.finite_product_derivative_geometric {ι : Type u_1} {E : Type u_2} {A : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedCommRing A] [NormedAlgebra ℝ A] [NormOneClass A] (u : Finset ι) (f : ι → E → A) (hf : ∀ j ∈ u, ContDiff ℝ (↑⊤) (f j)) (x : E) {m : ℕ} {R : ℝ} (hR : 0 ≤ R) (hfi : ∀ j ∈ u, ∀ i ≤ m, ‖iteratedFDeriv ℝ i (f j) x‖ ≤ R ^ i) : ‖iteratedFDeriv ℝ m (fun (y : E) => ∏ j ∈ u, f j y) x‖ ≤ (↑u.card * R) ^ m

A tensor product of unit zeroth derivatives has a dimension-to-the-order loss.

theorem TrilinearHT.Auto.coordinate_composition_derivative_norm {d : ℕ} {A : Type u_1} [NormedAddCommGroup A] [NormedSpace ℝ A] {f : ℝ → A} (hf : ContDiff ℝ (↑⊤) f) (i : Fin d) (z : Fin d → ℝ) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin d → ℝ) => f (y i)) z‖ ≤ ‖iteratedDeriv m f (z i)‖

Restricting to one coordinate cannot increase a derivative operator norm.

theorem TrilinearHT.Auto.coordinate_projection_derivative_norm {d : ℕ} (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) (i : Fin d) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin d → ℝ) => y i) z‖ ≤ 1

theorem TrilinearHT.Auto.coordinate_product_derivative_norm {d : ℕ} (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) (i j : Fin d) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin d → ℝ) => y i * y j) z‖ ≤ 2 ^ m

A product of two coordinates has geometric derivative bounds throughout the unit cube.

theorem TrilinearHT.Auto.bounded_quadratic_derivative_norm {d : ℕ} (C : Fin d → Fin d → ℝ) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin d → ℝ) => ∑ i : Fin d, ∑ j : Fin d, C i j * y i * y j) z‖ ≤ ↑d ^ 2 * 2 ^ m

Bounded quadratic coefficients give a uniform operator-derivative bound on the unit cube.

theorem TrilinearHT.Auto.bounded_quadratic_phase_derivative_norm {d : ℕ} (C : Fin d → Fin d → ℝ) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin d → ℝ) => ↑(Real.fourierChar (∑ i : Fin d, ∑ j : Fin d, C i j * y i * y j))) z‖ ≤ ↑m.factorial * (4 * Real.pi * (↑d + 1) ^ 2) ^ m

The Fourier exponential of a bounded quadratic has factorial-geometric derivatives on the unit cube; no horizontal frequencies or lattice basis occur in the bound.

theorem TrilinearHT.Auto.chartCoordinateProduct_derivative_geometric {d : ℕ} {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (z : Fin d → ℝ) {m : ℕ} {R : ℝ} (hR : 0 ≤ R) (hfi : ∀ i ≤ m, ∀ (x : ℝ), |iteratedDeriv i f x| ≤ R ^ i) : ‖iteratedFDeriv ℝ m (chartCoordinateProduct f) z‖ ≤ (↑d * R) ^ m

Uniform one-variable geometric bounds yield an operator-norm tensor cutoff bound.

theorem TrilinearHT.Auto.chart_restriction_derivative_norm {d D : ℕ} {f : (Fin d → ℝ) → ℂ} (hf : ContDiff ℝ (↑⊤) f) (s : Fin d → Fin D) (z : Fin D → ℝ) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : Fin D → ℝ) => f fun (i : Fin d) => y (s i)) z‖ ≤ ‖iteratedFDeriv ℝ m f fun (i : Fin d) => z (s i)‖

Coordinate restriction cannot increase an iterated derivative operator norm.

theorem TrilinearHT.Auto.bounded_quadratic_phase_derivative_geometric {d : ℕ} (C : Fin d → Fin d → ℝ) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) (m i : ℕ) (hi : i ≤ m) : ‖iteratedFDeriv ℝ i (fun (y : Fin d → ℝ) => ↑(Real.fourierChar (∑ j : Fin d, ∑ k : Fin d, C j k * y j * y k))) z‖ ≤ (4 * Real.pi * (↑d + 1) ^ 2 * (↑m + 1)) ^ i

theorem TrilinearHT.Auto.chartQuadraticAmplitude_derivative_geometric {d : ℕ} {f : ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (C : Fin d → Fin d → ℝ) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (z : Fin d → ℝ) (hz : ∀ (i : Fin d), |z i| ≤ 1) {m i : ℕ} (hi : i ≤ m) {R : ℝ} (hR : 0 ≤ R) (hfi : ∀ j ≤ m, ∀ (x : ℝ), |iteratedDeriv j f x| ≤ R ^ j) : ‖iteratedFDeriv ℝ i (chartQuadraticAmplitude f C) z‖ ≤ (↑d * R + 4 * Real.pi * (↑d + 1) ^ 2 * (↑m + 1)) ^ i

The quadratic cutoff has geometric bounds up to a chosen order inside the unit cube.

theorem TrilinearHT.Auto.localizedQuadraticChart_amplitude_support {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (hfs : ∀ (x : ℝ), 1 ≤ |x| → f x = 0) (hgs : ∀ (x : ℝ), 1 ≤ |x| → g x = 0) : tsupport (localizedQuadraticChart θ v ell C f g hf hg hfc hgc).amplitude ⊆ Metric.closedBall 0 1

The actual doubled amplitude and all its derivatives are supported in the unit cube.

theorem TrilinearHT.Auto.localizedQuadraticChart_amplitude_derivative_geometric {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) (hfs : ∀ (x : ℝ), 1 ≤ |x| → f x = 0) (hgs : ∀ (x : ℝ), 1 ≤ |x| → g x = 0) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (z : Fin (d + d) → ℝ) (m : ℕ) {R T : ℝ} (hR : 0 ≤ R) (hT : 0 ≤ T) (hfi : ∀ i ≤ m, ∀ (x : ℝ), |iteratedDeriv i f x| ≤ R ^ i) (hgi : ∀ i ≤ m, ∀ (x : ℝ), |iteratedDeriv i g x| ≤ T ^ i) : ‖iteratedFDeriv ℝ m (localizedQuadraticChart θ v ell C f g hf hg hfc hgc).amplitude z‖ ≤ (↑d * R + 4 * Real.pi * (↑d + 1) ^ 2 * (↑m + 1) + ↑d * T) ^ m

Operator-norm derivatives of the actual doubled chart amplitude have a uniform geometric bound. Compact support removes the need for any restriction on the evaluation point.

theorem TrilinearHT.Auto.gevrey_derivative_geometric (f : ℝ → ℝ) (K : ℕ) (hK : 1 ≤ K) (hunit : ∀ (x : ℝ), |f x| ≤ 1) (hderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i f x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) (m i : ℕ) (hi : i ≤ m) (x : ℝ) : |iteratedDeriv i f x| ≤ ((↑K * (↑m + 1)) ^ (2 * K)) ^ i

Unit zeroth derivatives remove the dimension-dependent loss in a Gevrey product.

theorem TrilinearHT.Auto.scaled_gevrey_derivative_geometric (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (K : ℕ) (hK : 1 ≤ K) (hunit : ∀ (x : ℝ), |f x| ≤ 1) (hderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i f x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) {r : ℝ} (hr : 0 < r) (m i : ℕ) (hi : i ≤ m) (x : ℝ) : |iteratedDeriv i (fun (y : ℝ) => f (y / r)) x| ≤ ((↑K * (↑m + 1)) ^ (2 * K) / r) ^ i

Scaling a unit cutoff contributes exactly one inverse-radius factor per derivative.

theorem TrilinearHT.Auto.local_chart_derivative_budget (d K m : ℕ) (hK : 1 ≤ K) {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) : (↑d * ((↑K * (↑m + 1)) ^ (2 * K) / r) + 4 * Real.pi * (↑d + 1) ^ 2 * (↑m + 1) + ↑d * (↑K * (↑m + 1)) ^ (2 * K)) ^ m ≤ (100 * (↑K + 1) * (↑d + 1) / r) ^ ((2 * K + 2) * (m + 1)) * (↑m + 1) ^ ((2 * K + 2) * (m + 1))

The geometric amplitude base fits one fixed Gevrey order, uniformly in dimension and radius.

theorem TrilinearHT.Auto.localizedQuadraticChart_gevrey_bound {d : ℕ} (θ v : Fin d → ℝ) (ell : ℝ) (C : Fin d → Fin d → ℝ) (f g : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (hfs : ∀ (x : ℝ), 1 ≤ |x| → f x = 0) (hgs : ∀ (x : ℝ), 1 ≤ |x| → g x = 0) (hC : ∀ (i j : Fin d), |C i j| ≤ 1) (K : ℕ) (hK : 1 ≤ K) (hfu : ∀ (x : ℝ), |f x| ≤ 1) (hgu : ∀ (x : ℝ), |g x| ≤ 1) (hfderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i f x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) (hgderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i g x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) (m : ℕ) (word : Fin m → Fin (d + d)) (z : Fin (d + d) → ℝ) : ‖coordinateWordDerivative m (localizedQuadraticChart θ v ell C (fun (x : ℝ) => f (x / r)) g ⋯ hg ⋯ hgc).amplitude word z‖ ≤ (100 * (↑K + 1) * (↑d + 1) / r) ^ ((2 * K + 2) * (m + 1)) * (↑m + 1) ^ ((2 * K + 2) * (m + 1))

Blueprint lem:local-chart, line 1082: the doubled amplitude has one fixed Gevrey order and explicit polynomial dependence on dimension and inverse radius.

theorem TrilinearHT.Auto.gevrey_derivative_bound_mono (f : ℝ → ℝ) {K L : ℕ} (hK : 1 ≤ K) (hKL : K ≤ L) (h : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i f x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) (i : ℕ) (x : ℝ) : |iteratedDeriv i f x| ≤ (↑L * (↑i + 1)) ^ (L * (i + 1))

noncomputable def TrilinearHT.Auto.modulateQuadraticChart {d : ℕ} (A : QuadraticChartData d) (b : ℝ) : QuadraticChartData d

Multiply a quadratic chart by a linear modulation of frequency b.

Equations

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

theorem TrilinearHT.Auto.modulateQuadraticChart_atom {d : ℕ} (A : QuadraticChartData d) (b y : ℝ) : quadraticChartAtom (modulateQuadraticChart A b) y = ↑(Real.fourierChar (b * y)) * quadraticChartAtom A y

theorem TrilinearHT.Auto.modulateQuadraticChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (b : ℝ) : QuadraticChartComplexity c₀ H (modulateQuadraticChart A b)

theorem TrilinearHT.Auto.modulateQuadraticChart_bounded {d : ℕ} {A : QuadraticChartData d} (hA : IsBoundedQuadraticChart A) (b : ℝ) : IsBoundedQuadraticChart (modulateQuadraticChart A b)

theorem TrilinearHT.Auto.translated_chart_power_budget {P X : ℝ} (hP : 100000 ≤ P) (n : ℕ) (hnP : ↑n ≤ P) (hX0 : 0 ≤ X) (hX : X ≤ P ^ 22) : chartTranslationBudget (Real.exp (↑n * X ^ n)) ≤ Real.exp (P ^ (66 * n + 4))

theorem TrilinearHT.Auto.uniform_translated_chart_budget (n : ℕ) (R : ℝ) (hR : 100000 ≤ R) (hnR : ↑n ≤ R) : ∃ (C : ℕ), 1 ≤ C ∧ ∀ (B : ℝ), 1 ≤ B → ∀ (X : ℝ), 0 ≤ X → X ≤ (R * B ^ 8) ^ 22 → chartTranslationBudget (Real.exp (↑n * X ^ n)) ≤ Real.exp (↑C * B ^ C) ∧ (R * B ^ 8) ^ 34 ≤ ↑C * B ^ C

The lattice model for a locally quadratic chart

@[reducible, inline]

noncomputable abbrev TrilinearHT.Auto.bohrLiftLattice {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) : Submodule ℤ (EuclideanSpace ℝ ↥S)

The full lift lattice of a Bohr frequency set. The frequency 1 is its distinguished coordinate; indexing by the set avoids an arbitrary ordering.

Equations

• TrilinearHT.Auto.bohrLiftLattice S hS = TrilinearHT.Auto.cyclicLiftLattice q (fun (s : ↥S) => ↑(↑s).val) ⟨1, hS⟩

noncomputable def TrilinearHT.Auto.bohrLiftProjection {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) : ↥(bohrLiftLattice S hS) →+ ZMod q

Project the integer Bohr-lift lattice onto its underlying cyclic group.

Equations

• TrilinearHT.Auto.bohrLiftProjection S hS = TrilinearHT.Auto.cyclicLiftProjection q (fun (s : ↥S) => ↑(↑s).val) ⟨1, hS⟩

theorem TrilinearHT.Auto.bohrLiftProjection_character {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (x : ↥(bohrLiftLattice S hS)) (s : ↥S) : ↑((↑x).ofLp s) = ZMod.toAddCircle (↑s * (bohrLiftProjection S hS) x)

Every lift coordinate modulo one is the corresponding Bohr character.

theorem TrilinearHT.Auto.integerCoefficientBox_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {n : ℕ} (e : E ≃ₗ[ℝ] F) (b : Module.Basis (Fin n) ℝ E) (I : Finset (Fin n)) (a : Fin n → ℤ) (x : E) : e x ∈ integerCoefficientBox (b.map e) I a ↔ x ∈ integerCoefficientBox b I a

Coefficient boxes commute with linear changes of basis.

theorem TrilinearHT.Auto.scaledSmallBallCoefficientBox {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} (hn : 0 < n) (b : Module.Basis (Fin n) ℝ E) {ρ : ℝ} (hρ : 0 < ρ) : ∃ (c : Module.Basis (Fin n) ℝ E) (I : Finset (Fin n)) (a : Fin n → ℤ), Submodule.span ℤ (Set.range ⇑c) = Submodule.span ℤ (Set.range ⇑b) ∧ (∀ i ∈ I, 1 ≤ a i) ∧ Metric.closedBall 0 (latticeBoxRadius n * ρ) ∩ ↑(Submodule.span ℤ (Set.range ⇑b)) ⊆ integerCoefficientBox c I a ∧ integerCoefficientBox c I a ⊆ Metric.closedBall 0 (ρ / 4) ∧ ∀ (z : Fin n → ℤ), (∀ i ∉ I, z i = 0) → (∀ i ∈ I, |z i| ≤ a i) → ∀ (J : Finset (Fin n)), ‖∑ i ∈ J, z i • c i‖ ≤ ρ / 4

Rescaling the coefficient-box theorem preserves its integer coordinates and every partial-sum bound; blueprint lem:local-chart, line 1041.

theorem TrilinearHT.Auto.bohrLiftProjection_mem {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (x : ↥(bohrLiftLattice S hS)) (hx : ‖↑x‖ < ρ) : (bohrLiftProjection S hS) x ∈ graphBohrSet S ρ

A short lift projects into the Bohr domain, coordinate by coordinate.

theorem TrilinearHT.Auto.bohr_coefficient_box {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) : ∃ (b : Module.Basis (Fin S.card) ℝ (EuclideanSpace ℝ ↥S)) (I : Finset (Fin S.card)) (a : Fin S.card → ℤ), Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS ∧ (∀ i ∈ I, 1 ≤ a i) ∧ Metric.closedBall 0 (latticeBoxRadius S.card * ρ) ∩ ↑(bohrLiftLattice S hS) ⊆ integerCoefficientBox b I a ∧ integerCoefficientBox b I a ⊆ Metric.closedBall 0 (ρ / 4) ∧ (∀ (z : Fin S.card → ℤ), (∀ i ∉ I, z i = 0) → (∀ i ∈ I, |z i| ≤ a i) → ∀ (J : Finset (Fin S.card)), ‖∑ i ∈ J, z i • b i‖ ≤ ρ / 4) ∧ (∀ (x : ↥(bohrLiftLattice S hS)), ‖↑x‖ ≤ ρ / 4 → (bohrLiftProjection S hS) x ∈ graphBohrSet S ρ) ∧ ∀ (x y : ↥(bohrLiftLattice S hS)), ↑x ∈ integerCoefficientBox b I a → ↑y ∈ integerCoefficientBox b I a → (bohrLiftProjection S hS) x = (bohrLiftProjection S hS) y → x = y

Blueprint lem:local-chart, line 1041: the rescaled full-basis coefficient box, including every partial-sum bound, Bohr projection, and injectivity of that projection.

noncomputable def TrilinearHT.Auto.bohrBasisVector {q n : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (i : Fin n) : ↥(bohrLiftLattice S hS)

A real basis vector, viewed as an element of its specified Bohr lift lattice.

Equations

• TrilinearHT.Auto.bohrBasisVector S hS b hb i = ⟨b i, ⋯⟩

noncomputable def TrilinearHT.Auto.bohrBasisFrequency {q n : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (i : Fin n) : ZMod q

The projected cyclic generators of a coefficient box.

Equations

• TrilinearHT.Auto.bohrBasisFrequency S hS b hb i = (TrilinearHT.Auto.bohrLiftProjection S hS) (TrilinearHT.Auto.bohrBasisVector S hS b hb i)

theorem TrilinearHT.Auto.bohr_box_local_additive {q n : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (hρ : 0 < ρ) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (I : Finset (Fin n)) (a : Fin n → ℤ) (ha : ∀ i ∈ I, 1 ≤ a i) (hbound : ∀ (w : Fin n → ℤ), (∀ i ∉ I, w i = 0) → (∀ i ∈ I, |w i| ≤ a i) → ‖∑ i : Fin n, w i • b i‖ ≤ ρ / 4) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (z : Fin n → ℤ) (hz0 : ∀ i ∉ I, z i = 0) (hza : ∀ i ∈ I, |z i| ≤ a i) : M (∑ i : Fin n, z i • bohrBasisFrequency S hS b hb i) = ∑ i : Fin n, z i • M (bohrBasisFrequency S hS b hb i)

Local additivity becomes the exact integer-coordinate linear formula on the source box.

theorem TrilinearHT.Auto.bohr_box_quadratic_phase {q n : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (hρ : 0 < ρ) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (I : Finset (Fin n)) (a : Fin n → ℤ) (ha : ∀ i ∈ I, 1 ≤ a i) (hbound : ∀ (w : Fin n → ℤ), (∀ i ∉ I, w i = 0) → (∀ i ∈ I, |w i| ≤ a i) → ‖∑ i : Fin n, w i • b i‖ ≤ ρ / 4) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (z : Fin n → ℤ) (hz0 : ∀ i ∉ I, z i = 0) (hza : ∀ i ∈ I, |z i| ≤ a i) : have v := bohrBasisFrequency S hS b hb; ZMod.toAddCircle (M (∑ i : Fin n, z i • v i) * ∑ i : Fin n, z i • v i) = ↑(((∑ i : Fin n, ↑(z i) * ↑(M (v i)).val) * ∑ i : Fin n, ↑(z i) * ↑(v i).val) / ↑q)

Blueprint lem:local-chart, lines 1043-1052: on the entire coefficient box the phase is the displayed ordinary quadratic polynomial, with the standard integer representatives.

noncomputable def TrilinearHT.Auto.bohrLiftDirection {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) : ↥(bohrLiftLattice S hS)

The distinguished rational direction generating the cyclic quotient.

Equations

• TrilinearHT.Auto.bohrLiftDirection S hS = (Module.Basis.restrictScalars ℤ (TrilinearHT.Auto.cyclicLiftBasis q (fun (s : ↥S) => ↑(↑s).val) ⟨1, hS⟩)) ⟨1, hS⟩

theorem TrilinearHT.Auto.bohrLiftDirection_projection {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) : (bohrLiftProjection S hS) (bohrLiftDirection S hS) = 1

theorem TrilinearHT.Auto.bohr_integer_dual_coordinates {q n : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (b : Module.Basis (Fin n) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) : ∃ (U : Fin n → ↥S → ℤ) (t : Fin n → ℤ), (∀ (i : Fin n) (s : ↥S), ((euclideanDualBasis b) i).ofLp s = ↑(U i s)) ∧ (∀ (i : Fin n), inner ℝ ((euclideanDualBasis b) i) ↑(bohrLiftDirection S hS) = ↑(t i)) ∧ (∀ (x : EuclideanSpace ℝ ↥S) (i : Fin n), (b.repr x) i = ∑ s : ↥S, ↑(U i s) * x.ofLp s) ∧ ∀ (m : ℤ) (k : ↥S → ℤ) (i : Fin n), (b.repr (m • ↑(bohrLiftDirection S hS) - WithLp.toLp 2 fun (s : ↥S) => ↑(k s))) i = ↑(t i * m - ∑ s : ↥S, U i s * k s)

The source integer dual-coordinate forms for the distinguished Bohr lift direction.

noncomputable def TrilinearHT.Auto.bohrCenteredLift {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (n : ℤ) : EuclideanSpace ℝ ↥S

The centered real representatives of all characters at an integer point.

Equations

• TrilinearHT.Auto.bohrCenteredLift S n = WithLp.toLp 2 fun (s : ↥S) => TrilinearHT.Auto.unitCircleCentered (ZMod.toAddCircle (↑s * ↑n))

theorem TrilinearHT.Auto.bohrCenteredLift_coord {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (n : ℤ) {r : ℝ} (hn : ↑n ∈ graphBohrSet S r) (s : ↥S) : |(bohrCenteredLift S n).ofLp s| < r

theorem TrilinearHT.Auto.bohrCenteredLift_norm {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (n : ℤ) {r : ℝ} (hr : 0 ≤ r) (hn : ↑n ∈ graphBohrSet S r) : ‖bohrCenteredLift S n‖ ≤ √↑S.card * r

theorem TrilinearHT.Auto.bohrCenteredLift_integer_difference {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (n : ℤ) : ∃ (k : ↥S → ℤ), bohrCenteredLift S n = n • ↑(bohrLiftDirection S hS) - WithLp.toLp 2 fun (s : ↥S) => ↑(k s)

The centered lift differs from the rational direction by an integer vector.

theorem TrilinearHT.Auto.bohrCenteredLift_mem {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (n : ℤ) : bohrCenteredLift S n ∈ bohrLiftLattice S hS

theorem TrilinearHT.Auto.bohrCenteredLift_projection {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (n : ℤ) : (bohrLiftProjection S hS) ⟨bohrCenteredLift S n, ⋯⟩ = ↑n

theorem TrilinearHT.Auto.bohr_supported_lift_in_box {q d : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (cutoff : ℝ → ℝ) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) {r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hsmall : r ≤ latticeBoxRadius S.card * ρ / (2 * √↑S.card)) (b : Module.Basis (Fin d) ℝ (EuclideanSpace ℝ ↥S)) (I : Finset (Fin d)) (a : Fin d → ℤ) (hbox : Metric.closedBall 0 (latticeBoxRadius S.card * ρ) ∩ ↑(bohrLiftLattice S hS) ⊆ integerCoefficientBox b I a) (n : ℤ) (hn : graphBohrWeight cutoff S r ↑n ≠ 0) : (∀ (s : ↥S), |(bohrCenteredLift S n).ofLp s| < r) ∧ ‖bohrCenteredLift S n‖ ≤ latticeBoxRadius S.card * ρ / 2 ∧ bohrCenteredLift S n ∈ integerCoefficientBox b I a

The supporting Bohr lift lies in the small lattice ball and hence in the source box.

theorem TrilinearHT.Auto.unitCircle_fract_mul_int (a : ℝ) (z : ℤ) : ↑(Int.fract a * ↑z) = ↑(a * ↑z)

Integer monomials do not distinguish a coefficient from its fractional part.

theorem TrilinearHT.Auto.quadratic_integer_coefficient_reduction {ι : Type u_1} [Fintype ι] (ell : ℝ) (b : ι → ℝ) (C : ι → ι → ℝ) : ∃ (b' : ι → ℝ) (C' : ι → ι → ℝ), (∀ (i : ι), |b' i| ≤ 1) ∧ (∀ (i j : ι), |C' i j| ≤ 1) ∧ ∀ (n : ℤ) (k : ι → ℤ), ↑(ell * ↑n ^ 2 + ↑n * ∑ i : ι, b' i * ↑(k i) + ∑ i : ι, ∑ j : ι, C' i j * ↑(k i) * ↑(k j)) = ↑(ell * ↑n ^ 2 + ↑n * ∑ i : ι, b i * ↑(k i) + ∑ i : ι, ∑ j : ι, C i j * ↑(k i) * ↑(k j))

Reducing mixed and lattice-quadratic coefficients modulo one preserves the phase at every integer input; blueprint lem:local-chart, lines 1058-1062.

theorem TrilinearHT.Auto.linear_product_quadratic_expansion {ι : Type u_1} [Fintype ι] (a d c n : ℝ) (u v k : ι → ℝ) : (a * n + ∑ i : ι, u i * k i) * (d * n + ∑ i : ι, v i * k i) * c = a * d * c * n ^ 2 + n * ∑ i : ι, (a * v i + d * u i) * c * k i + ∑ i : ι, ∑ j : ι, u i * v j * c * k i * k j

Algebraic expansion of a product of linear forms into the source quadratic shape.

theorem TrilinearHT.Auto.integer_linear_form_substitution {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (t : ι → ℤ) (U : ι → κ → ℤ) (m : ι → ℝ) (n : ℤ) (k : κ → ℤ) : ∑ i : ι, ↑(t i * n - ∑ j : κ, U i j * k j) * m i = (∑ i : ι, ↑(t i) * m i) * ↑n + ∑ j : κ, (-∑ i : ι, ↑(U i j) * m i) * ↑(k j)

Substituting an integer linear vector into a real linear form.

theorem TrilinearHT.Auto.quadratic_horizontal_substitution {ι : Type u_1} [Fintype ι] (ell : ℝ) (b : ι → ℝ) (C : ι → ι → ℝ) (θ : ι → ℝ) : ∃ (ell' : ℝ) (v : ι → ℝ), (∀ (i : ι), v i = -b i - ∑ j : ι, (C i j + C j i) * θ j) ∧ ∀ (n : ℝ) (w : ι → ℝ), ell * n ^ 2 + n * ∑ i : ι, b i * (θ i * n - w i) + ∑ i : ι, ∑ j : ι, C i j * (θ i * n - w i) * (θ j * n - w j) = ell' * n ^ 2 + n * ∑ i : ι, v i * w i + ∑ i : ι, ∑ j : ι, C i j * w i * w j

The real substitution used for the enlarged chart: all possibly large coefficients enter only the outside phase or the horizontal vector.

theorem TrilinearHT.Auto.integer_linear_quadratic_reduction {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (t : ι → ℤ) (U : ι → κ → ℤ) (m v : ι → ℝ) (Q : ℝ) : ∃ (ell : ℝ) (b : κ → ℝ) (C : κ → κ → ℝ), (∀ (j : κ), |b j| ≤ 1) ∧ (∀ (i j : κ), |C i j| ≤ 1) ∧ ∀ (n : ℤ) (k : κ → ℤ), ↑(((∑ i : ι, ↑(t i * n - ∑ j : κ, U i j * k j) * m i) * ∑ i : ι, ↑(t i * n - ∑ j : κ, U i j * k j) * v i) / Q) = ↑(ell * ↑n ^ 2 + ↑n * ∑ i : κ, b i * ↑(k i) + ∑ i : κ, ∑ j : κ, C i j * ↑(k i) * ↑(k j))

Substituting the integral dual forms and reducing coefficients gives a bounded matrix, uniformly in all original coefficients; blueprint lem:local-chart, lines 1058-1062.

theorem TrilinearHT.Auto.integer_linear_quadratic_horizontal {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (t : ι → ℤ) (U : ι → κ → ℤ) (m v : ι → ℝ) (Q : ℝ) (θ : κ → ℝ) : ∃ (ell : ℝ) (h : κ → ℝ) (C : κ → κ → ℝ), (∀ (i j : κ), |C i j| ≤ 1) ∧ ∀ (n : ℤ) (k : κ → ℤ), ↑(((∑ i : ι, ↑(t i * n - ∑ j : κ, U i j * k j) * m i) * ∑ i : ι, ↑(t i * n - ∑ j : κ, U i j * k j) * v i) / Q) = ↑(ell * ↑n ^ 2 + ↑n * ∑ i : κ, h i * (θ i * ↑n - ↑(k i)) + ∑ i : κ, ∑ j : κ, C i j * (θ i * ↑n - ↑(k i)) * (θ j * ↑n - ↑(k j)))

The integral dual-coordinate quadratic becomes a real horizontal phase with a coefficientwise bounded amplitude matrix; blueprint lem:local-chart, lines 1058-1067.

theorem TrilinearHT.Auto.bohr_box_phase_coordinates {q d : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (hρ : 0 < ρ) (b : Module.Basis (Fin d) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (I : Finset (Fin d)) (a : Fin d → ℤ) (ha : ∀ i ∈ I, 1 ≤ a i) (hbound : ∀ (z : Fin d → ℤ), (∀ i ∉ I, z i = 0) → (∀ i ∈ I, |z i| ≤ a i) → ‖∑ i : Fin d, z i • b i‖ ≤ ρ / 4) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (x : ↥(bohrLiftLattice S hS)) (hx : ↑x ∈ integerCoefficientBox b I a) : ZMod.toAddCircle (M ((bohrLiftProjection S hS) x) * (bohrLiftProjection S hS) x) = ↑(((∑ i : Fin d, (b.repr ↑x) i * ↑(M (bohrBasisFrequency S hS b hb i)).val) * ∑ i : Fin d, (b.repr ↑x) i * ↑(bohrBasisFrequency S hS b hb i).val) / ↑q)

The local quadratic phase in the actual real basis coordinates of a box point.

theorem TrilinearHT.Auto.bohr_local_quadratic_horizontal {q d : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {ρ : ℝ} (hρ : 0 < ρ) (b : Module.Basis (Fin d) ℝ (EuclideanSpace ℝ ↥S)) (hb : Submodule.span ℤ (Set.range ⇑b) = bohrLiftLattice S hS) (I : Finset (Fin d)) (a : Fin d → ℤ) (ha : ∀ i ∈ I, 1 ≤ a i) (hbound : ∀ (z : Fin d → ℤ), (∀ i ∉ I, z i = 0) → (∀ i ∈ I, |z i| ≤ a i) → ‖∑ i : Fin d, z i • b i‖ ≤ ρ / 4) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) : ∃ (ell : ℝ) (h : ↥S → ℝ) (C : ↥S → ↥S → ℝ), (∀ (i j : ↥S), |C i j| ≤ 1) ∧ ∀ (n : ℤ), bohrCenteredLift S n ∈ integerCoefficientBox b I a → ZMod.toAddCircle (M ↑n * ↑n) = ↑(ell * ↑n ^ 2 + ↑n * ∑ i : ↥S, h i * (bohrCenteredLift S n).ofLp i + ∑ i : ↥S, ∑ j : ↥S, C i j * (bohrCenteredLift S n).ofLp i * (bohrCenteredLift S n).ofLp j)

Blueprint lem:local-chart, lines 1054-1067: on every centered lift in the coefficient box, the original locally quadratic phase has the bounded-matrix horizontal form. The bounds are independent of the lattice basis and the modulus.

noncomputable def TrilinearHT.Auto.bohrFrequencyEquiv {q : ℕ} (S : Finset (ZMod q)) : Fin S.card ≃ ↥S

A finite enumeration used only to present Bohr coordinates in the chart convention.

Equations

• TrilinearHT.Auto.bohrFrequencyEquiv S = (Fintype.equivFinOfCardEq ⋯).symm

noncomputable def TrilinearHT.Auto.bohrLocalQuadraticChart {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) {r : ℝ} (hr : 0 < r) : QuadraticChartData (S.card + S.card)

The actual rational chart built from the local phase coefficients and the fixed Gevrey partition; blueprint lem:local-chart, lines 1069-1076.

Equations

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

theorem TrilinearHT.Auto.bohrLocalQuadraticChart_matrix_height {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) {r : ℝ} (hr : 0 < r) (i j : Fin (S.card + S.card)) : chartRationalHeight ((bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr).matrix i j) = 1

theorem TrilinearHT.Auto.bohrCenteredLift_weight {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (cutoff : ℝ → ℝ) (r : ℝ) (n : ℤ) : ∏ i : Fin S.card, ↑(cutoff ((bohrCenteredLift S n).ofLp ((bohrFrequencyEquiv S) i) / r)) = ↑(graphBohrWeight cutoff S r ↑n)

theorem TrilinearHT.Auto.bohrLocalQuadraticChart_bounded {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (hunit : ∀ (x : ℝ), |cutoff x| ≤ 1) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 2) : IsBoundedQuadraticChart (bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr)

theorem TrilinearHT.Auto.bohrLocalQuadraticChart_integer_formula {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) {r : ℝ} (hr : 0 < r) (hrsmall : r < 1 / 2) (n : ℤ) : quadraticChartAtom (bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr) ↑n = ↑(graphBohrWeight cutoff S r ↑n) * ↑(Real.fourierChar (ell * ↑n ^ 2 + ↑n * ∑ s : ↥S, v s * (bohrCenteredLift S n).ofLp s + ∑ s : ↥S, ∑ t : ↥S, C s t * (bohrCenteredLift S n).ofLp s * (bohrCenteredLift S n).ofLp t))

Exact integer formula for the constructed chart, including its zero-weight values.

theorem TrilinearHT.Auto.cyclic_character_of_real_phase {q : ℕ} [NeZero q] (x : ZMod q) (t : ℝ) (h : ZMod.toAddCircle x = ↑t) : ZMod.stdAddChar x = ↑(Real.fourierChar t)

theorem TrilinearHT.Auto.local_chart_radius_lt_half {q : ℕ} (S : Finset (ZMod q)) (hS : 1 ∈ S) {r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hsmall : r ≤ latticeBoxRadius S.card * ρ / (2 * √↑S.card)) : r < 1 / 2

theorem TrilinearHT.Auto.bohr_local_chart_bounded_values {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) {r ρ : ℝ} (hr : 0 < r) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hsmall : r ≤ latticeBoxRadius S.card * ρ / (2 * √↑S.card)) (M : ZMod q → ZMod q) (hadd : ∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (hunit : ∀ (x : ℝ), |cutoff x| ≤ 1) : ∃ (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ), (∀ (i j : ↥S), |C i j| ≤ 1) ∧ IsBoundedQuadraticChart (bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr) ∧ ∀ (n : ℤ), quadraticChartAtom (bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr) ↑n = ↑(graphBohrWeight cutoff S r ↑n) * ZMod.stdAddChar (M ↑n * ↑n)

Blueprint lem:local-chart, line 1078: the constructed chart is globally bounded and realizes the original weighted local phase at every integer, including zero weights. Quantitative derivative complexity is established separately.

theorem TrilinearHT.Auto.bohrLocalQuadraticChart_uniform_gevrey_bound (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (hunit : ∀ (x : ℝ), |cutoff x| ≤ 1) (K : ℕ) (hK : 1 ≤ K) (hderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i cutoff x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) : ∃ (L : ℕ), 1 ≤ L ∧ ∀ (q : ℕ) [inst : NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (C : ↥S → ↥S → ℝ), (∀ (i j : ↥S), |C i j| ≤ 1) → ∀ (r : ℝ) (hr : 0 < r), r ≤ 1 → ∀ (m : ℕ) (word : Fin m → Fin (S.card + S.card)) (z : Fin (S.card + S.card) → ℝ), ‖coordinateWordDerivative m (bohrLocalQuadraticChart S hS ell v C cutoff hf hsupp hr).amplitude word z‖ ≤ (100 * (↑L + 1) * (↑S.card + 1) / r) ^ ((2 * L + 2) * (m + 1)) * (↑m + 1) ^ ((2 * L + 2) * (m + 1))

One fixed Gevrey order controls all Bohr charts built from the given source cutoff. The order is chosen before the modulus, frequency set, radius and local phase.

theorem TrilinearHT.Auto.local_chart_complexity_parameter (L d C : ℕ) (hL : 1 ≤ L) (hCbound : 1000 * (L + 1) ≤ C) {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) : have H := Real.exp (↑C * (↑d + Real.log (1 / r) + 1) ^ C); Real.exp 2 ≤ H ∧ ↑(d + d) ≤ Real.log H ∧ 100 * (↑L + 1) * (↑d + 1) / r ≤ H

An explicit source-format complexity parameter controls dimension, support and derivatives.

theorem TrilinearHT.Auto.bohrLocalQuadraticChart_amplitude_support {q : ℕ} [NeZero q] (S : Finset (ZMod q)) (hS : 1 ∈ S) (ell : ℝ) (v : ↥S → ℝ) (Q : ↥S → ↥S → ℝ) (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) {r : ℝ} (hr : 0 < r) (hr1 : r ≤ 1) : tsupport (bohrLocalQuadraticChart S hS ell v Q cutoff hf hsupp hr).amplitude ⊆ Metric.closedBall 0 1

theorem TrilinearHT.Auto.locally_quadratic_chart (cutoff : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) cutoff) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (hunit : ∀ (x : ℝ), |cutoff x| ≤ 1) (K : ℕ) (hK : 1 ≤ K) (hderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i cutoff x| ≤ (↑K * (↑i + 1)) ^ (K * (i + 1))) : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (q : ℕ) [inst : NeZero q] (S : Finset (ZMod q)), 1 ∈ S → ∀ (r ρ : ℝ), 0 < r → 0 < ρ → ρ < 1 / 100 → r ≤ latticeBoxRadius S.card * ρ / (2 * √↑S.card) → ∀ (M : ZMod q → ZMod q), (∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) → ∃ (A : QuadraticChartData (S.card + S.card)), (∀ (i j : Fin (S.card + S.card)), chartRationalHeight (A.matrix i j) = 1) ∧ QuadraticChartComplexity c₀ (Real.exp (↑C * (↑S.card + Real.log (1 / r) + 1) ^ C)) A ∧ IsBoundedQuadraticChart A ∧ ∀ (n : ℤ), quadraticChartAtom A ↑n = ↑(graphBohrWeight cutoff S r ↑n) * ZMod.stdAddChar (M ↑n * ↑n)

Blueprint lem:local-chart, lines 1019-1084: every locally quadratic phase on the source Bohr domain is represented by a globally bounded real chart on the smaller weighted domain. The matrix has height one, and a fixed Gevrey order and one quasipolynomial budget work uniformly in the modulus, frequency set and local phase.

theorem TrilinearHT.Auto.bohr_initial_derivative_correlation {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (H S : Finset (ZMod q)) (ξ M : ZMod q → ZMod q) (f : ZMod q → ℂ) {ρ δ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1 / 100) (hδ : 0 < δ) (hH : 0 < ↑H.card / ↑q) (hadd : ∀ u ∈ graphBohrSet S ρ, ∀ v ∈ graphBohrSet S ρ, u + v ∈ graphBohrSet S ρ → M (u + v) = M u + M v) (hdiff : ∀ u ∈ H, ∀ v ∈ H, u - v ∈ graphBohrSet S ρ → ξ u - ξ v = 2 * M (u - v)) (hcor : ∀ h ∈ H, δ ^ 4 / √2 ≤ ‖finiteFourier (fun (x : ZMod q) => f (x + h) * (starRingEnd ℂ) (f x)) (ξ h)‖) : have ζ := δ ^ 4 * (↑H.card / ↑q) * graphBohrMass cutoff S (ρ / 100) / √2; 0 < ζ ∧ ∃ (x₀ : ZMod q) (ξ₀ : ZMod q) (c : ZMod q → ℂ), (∀ (h : ZMod q), ‖c h‖ ≤ 1) ∧ ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S (ρ / 100)) M (fun (x : ZMod q) => f (x + x₀)) (fun (x : ZMod q) => (starRingEnd ℂ) (f x) * ZMod.stdAddChar (-(ξ₀ * x))) c‖

theorem TrilinearHT.Auto.bohr_initial_correlation_log {q : ℕ} [NeZero q] (cutoff : ℝ → ℝ) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (H S : Finset (ZMod q)) {ρ δ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1 / 100) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hH : δ ^ 87112 / localFrequencyDensityCost ≤ ↑H.card / ↑q) (hrank : ↑S.card + Real.log (1 / ρ) ≤ 10 ^ 50 * (1 + Real.log (1 / δ)) ^ 4) : Real.log (1 / (δ ^ 4 * (↑H.card / ↑q) * graphBohrMass cutoff S (ρ / 100) / √2)) ≤ (localFrequencyDensityCost + 10 ^ 102) * (1 + Real.log (1 / δ)) ^ 8

theorem TrilinearHT.Auto.finite_inverse_radius (D d : ℕ) (hd : 0 < d) (hdD : d ≤ D) {ρ t ζ C : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (ht : 0 < t) (ht1 : t ≤ 1) (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (hC : 1 ≤ C) : ∃ (r : ℝ), 0 < r ∧ r ≤ t / 100 ∧ r ≤ latticeBoxRadius D * (ρ / 10) / (2 * √↑D) ∧ r ≤ ζ * (ρ / 100) / (100 * C * ↑d) ∧ Real.log (1 / r) ≤ Real.log (1 / t) + Real.log (1 / ζ) + 2 * Real.log (1 / ρ) + Real.log C + 20000 * (↑D + 1) ^ 2

theorem TrilinearHT.Auto.bohr_symmetry_refinement (cutoff : ℝ → ℝ) (hcont : ContDiff ℝ 1 cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) : ∃ (K : ℝ), 0 < K ∧ ∀ (q : ℕ) [inst : NeZero q], Odd q → ∀ (S : Finset (ZMod q)), 1 ∈ S → ∀ (ρ ζ C : ℝ), 0 < ρ → ρ < 1 / 100 → 0 < ζ → ζ ≤ 1 → 1 ≤ C → ∀ (M : ZMod q → ZMod q), (∀ x ∈ graphBohrSet S ρ, ∀ y ∈ graphBohrSet S ρ, x + y ∈ graphBohrSet S ρ → M (x + y) = M x + M y) → ∀ (a b c : ZMod q → ℂ), (∀ (x : ZMod q), ‖a x‖ ≤ 1) → (∀ (x : ZMod q), ‖b x‖ ≤ 1) → (∀ (x : ZMod q), ‖c x‖ ≤ 1) → ζ ≤ ‖graphLocalCorrelation (graphBohrWeight cutoff S (ρ / 100)) M a b c‖ → ∃ (T : Finset (ZMod q)) (t : ℝ) (r : ℝ), S ⊆ T ∧ 1 ∈ T ∧ 0 < t ∧ t < ρ / 100 ∧ ↑T.card + Real.log (1 / t) ≤ K * graphSymmetryBudget S.card (ρ / 100) ζ ^ 8 ∧ 0 < r ∧ r ≤ t / 100 ∧ r ≤ latticeBoxRadius T.card * (ρ / 10) / (2 * √↑T.card) ∧ r ≤ ζ * (ρ / 100) / (100 * C * ↑S.card) ∧ (∀ x ∈ graphBohrSet T r, ∀ y ∈ graphBohrSet T r, ‖graphAlternatingPhase M x y‖ ≤ ζ / 1000) ∧ (∀ x ∈ graphBohrSet T (ρ / 10), ∀ y ∈ graphBohrSet T (ρ / 10), x + y ∈ graphBohrSet T (ρ / 10) → M (x + y) = M x + M y) ∧ Real.log (1 / r) ≤ Real.log (1 / t) + Real.log (1 / ζ) + 2 * Real.log (1 / ρ) + Real.log C + 20000 * (↑T.card + 1) ^ 2

theorem TrilinearHT.Auto.cyclic_linear_phase_real {q : ℕ} [NeZero q] (ℓ : ZMod q) : ∃ (b : ℝ), ∀ (n : ℤ), ZMod.stdAddChar (-ℓ * ↑n) = ↑(Real.fourierChar (b * ↑n))

theorem TrilinearHT.Auto.quadratic_chart_of_weighted_phase {q : ℕ} [NeZero q] {d c₀ : ℕ} {H η : ℝ} (hc : 1 ≤ c₀) (w : ZMod q → ℝ) (M : ZMod q → ZMod q) (f : ZMod q → ℂ) (y ℓ : ZMod q) (A : QuadraticChartData d) (hA : QuadraticChartComplexity c₀ H A) (hbounded : IsBoundedQuadraticChart A) (hvalues : ∀ (n : ℤ), quadraticChartAtom A ↑n = ↑(w ↑n) * ZMod.stdAddChar (M ↑n * ↑n)) (hcorr : η ≤ ‖Finset.univ.expect fun (u : ZMod q) => ↑(w u) * f (u + y) * ZMod.stdAddChar (-(M u * u) + ℓ * u)‖) : ∃ (B : QuadraticChartData d), QuadraticChartComplexity c₀ (chartTranslationBudget H) B ∧ IsBoundedQuadraticChart B ∧ η ≤ ‖Finset.univ.expect fun (n : ZMod q) => f n * (starRingEnd ℂ) (quadraticChartAtom B ↑n.val)‖

theorem TrilinearHT.Auto.finite_inverse_with_cutoff (cutoff : ℝ → ℝ) (hcut : ContDiff ℝ (↑⊤) cutoff) (hb0 : ∀ (x : ℝ), 0 ≤ cutoff x) (hb1 : ∀ (x : ℝ), cutoff x ≤ 1) (hbone : ∀ (x : ℝ), |x| ≤ 1 / 2 → cutoff x = 1) (hsupp : ∀ (x : ℝ), 1 ≤ |x| → cutoff x = 0) (k : ℕ) (hk : 1 ≤ k) (hderiv : ∀ (i : ℕ) (x : ℝ), |iteratedDeriv i cutoff x| ≤ (↑k * (↑i + 1)) ^ (k * (i + 1))) : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (q : ℕ) [inst : NeZero q], Odd q → ∀ (δ : ℝ), 0 < δ → δ < 1 / 2 → ∀ (f : ZMod q → ℂ), (∀ (x : ZMod q), ‖f x‖ ≤ 1) → δ ≤ gowersNorm (finiteHaar (ZMod q)) 3 f → ∃ (d : ℕ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C)) A ∧ IsBoundedQuadraticChart A ∧ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C))⁻¹ ≤ ‖Finset.univ.expect fun (x : ZMod q) => f x * (starRingEnd ℂ) (quadraticChartAtom A ↑x.val)‖

theorem TrilinearHT.Auto.finite_inverse : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (q : ℕ) [inst : NeZero q], Odd q → ∀ (δ : ℝ), 0 < δ → δ < 1 / 2 → ∀ (f : ZMod q → ℂ), (∀ (x : ZMod q), ‖f x‖ ≤ 1) → δ ≤ gowersNorm (finiteHaar (ZMod q)) 3 f → ∃ (d : ℕ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C)) A ∧ IsBoundedQuadraticChart A ∧ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C))⁻¹ ≤ ‖Finset.univ.expect fun (x : ZMod q) => f x * (starRingEnd ℂ) (quadraticChartAtom A ↑x.val)‖

Blueprint thm:finite-inverse, lines 1088-1159. One fixed Gevrey order and one quasipolynomial budget work for every positive odd modulus and every bounded input with the stated U3 lower bound. In particular this covers all odd q at least three.