Section 3: Local forms, finite constants, and stopping

This file was automatically generated by Claude.

Formalization of blueprint Section 3, "Local forms, finite constants, and stopping" (sec:reduction, lines 363-468) of blueprint/formalization_blueprint.tex.

def TrilinearHT.Auto.reciprocalExponentPolytope (d k : ℕ) : Set (Fin d → ℝ)

The reciprocal exponent polytope in blueprint lem:absolute, line 390.

Equations

• TrilinearHT.Auto.reciprocalExponentPolytope d k = {a : Fin d → ℝ | (∀ (i : Fin d), 0 ≤ a i ∧ a i ≤ 1) ∧ ∑ i : Fin d, a i ≤ ↑k}

theorem TrilinearHT.Auto.reciprocalExponentPolytope_convex (d k : ℕ) : Convex ℝ (reciprocalExponentPolytope d k)

theorem TrilinearHT.Auto.reciprocalExponentPolytope_compact (d k : ℕ) : IsCompact (reciprocalExponentPolytope d k)

theorem TrilinearHT.Auto.extremePoint_perturbation_eq_zero {d : ℕ} {s : Set (Fin d → ℝ)} {a v : Fin d → ℝ} (ha : a ∈ Set.extremePoints ℝ s) (hplus : a + v ∈ s) (hminus : a - v ∈ s) : v = 0

A nonzero symmetric perturbation rules out an extreme point.

theorem TrilinearHT.Auto.reciprocalExponentPolytope_perturb {d k : ℕ} {a v : Fin d → ℝ} (hv : ∀ (i : Fin d), |v i| ≤ min (a i) (1 - a i)) (hs : |∑ i : Fin d, v i| ≤ ↑k - ∑ i : Fin d, a i) : a + v ∈ reciprocalExponentPolytope d k ∧ a - v ∈ reciprocalExponentPolytope d k

theorem TrilinearHT.Auto.reciprocalExponentPolytope_extreme_fractional_unique {d k : ℕ} {a : Fin d → ℝ} (ha : a ∈ Set.extremePoints ℝ (reciprocalExponentPolytope d k)) {i j : Fin d} (hi : 0 < a i ∧ a i < 1) (hj : 0 < a j ∧ a j < 1) : i = j

Two fractional coordinates admit opposite perturbations, as in blueprint lem:absolute, line 390.

theorem TrilinearHT.Auto.reciprocalExponentPolytope_extreme_fractional_sum {d k : ℕ} {a : Fin d → ℝ} (ha : a ∈ Set.extremePoints ℝ (reciprocalExponentPolytope d k)) {i : Fin d} (hi : 0 < a i ∧ a i < 1) : ∑ t : Fin d, a t = ↑k

theorem TrilinearHT.Auto.reciprocalExponentPolytope_extreme_boolean {d k : ℕ} {a : Fin d → ℝ} (ha : a ∈ Set.extremePoints ℝ (reciprocalExponentPolytope d k)) (i : Fin d) : a i = 0 ∨ a i = 1

Every extreme point of the reciprocal exponent polytope is Boolean.

def TrilinearHT.Auto.reciprocalExponentEndpoints (d k : ℕ) : Set (Fin d → ℝ)

Boolean endpoint configurations with at most k occupied slots.

Equations

• TrilinearHT.Auto.reciprocalExponentEndpoints d k = {a : Fin d → ℝ | (∀ (i : Fin d), a i = 0 ∨ a i = 1) ∧ ∑ i : Fin d, a i ≤ ↑k}

theorem TrilinearHT.Auto.reciprocalExponentEndpoints_finite (d k : ℕ) : (reciprocalExponentEndpoints d k).Finite

theorem TrilinearHT.Auto.reciprocalExponentPolytope_eq_convexHull (d k : ℕ) : reciprocalExponentPolytope d k = (convexHull ℝ) (reciprocalExponentEndpoints d k)

Blueprint lem:absolute, line 390: the admissible reciprocal exponents are precisely the convex hull of Boolean configurations with at most k ones. In particular d = 4, k = 2 gives the source interpolation polytope.

theorem TrilinearHT.Auto.ennreal_product_convex_exponents {d : ℕ} (f : Fin d → ENNReal) {a b : Fin d → ℝ} (ha : ∀ (i : Fin d), 0 ≤ a i) (hb : ∀ (i : Fin d), 0 ≤ b i) {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : ∏ i : Fin d, f i ^ (s * a i + t * b i) = (∏ i : Fin d, f i ^ a i) ^ s * (∏ i : Fin d, f i ^ b i) ^ t

Product identity used by positive Hölder interpolation, valid also for zero and infinite bases because every exponent is nonnegative.

theorem TrilinearHT.Auto.positiveExponentBound_convex {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {d : ℕ} (f : Fin d → X → ENNReal) (hf : ∀ (i : Fin d), AEMeasurable (f i) μ) (B : Fin d → ENNReal) (C : ENNReal) : Convex ℝ {a : Fin d → ℝ | (∀ (i : Fin d), 0 ≤ a i) ∧ ∫⁻ (x : X), ∏ i : Fin d, f i x ^ a i ∂μ ≤ C * ∏ i : Fin d, B i ^ a i}

Positive product-integral bounds form a convex set of nonnegative exponents. This is the Hölder interpolation step of lem:absolute, line 392.

theorem TrilinearHT.Auto.positiveEndpointInterpolation {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) {d k : ℕ} (f : Fin d → X → ENNReal) (hf : ∀ (i : Fin d), AEMeasurable (f i) μ) (B : Fin d → ENNReal) (C : ENNReal) (hend : ∀ a ∈ reciprocalExponentEndpoints d k, ∫⁻ (x : X), ∏ i : Fin d, f i x ^ a i ∂μ ≤ C * ∏ i : Fin d, B i ^ a i) {a : Fin d → ℝ} (ha : a ∈ reciprocalExponentPolytope d k) : ∫⁻ (x : X), ∏ i : Fin d, f i x ^ a i ∂μ ≤ C * ∏ i : Fin d, B i ^ a i

Blueprint lem:absolute, line 392: positive Boolean endpoint estimates interpolate throughout the complete reciprocal-exponent polytope. The extended nonnegative formulation includes zero and infinite integrals without division.

theorem TrilinearHT.Auto.real_lintegral_affine (g : ℝ → ENNReal) (hg : Measurable g) {a : ℝ} (ha : a ≠ 0) (b : ℝ) : ∫⁻ (t : ℝ), g (b + a * t) = ENNReal.ofReal |a⁻¹| * ∫⁻ (u : ℝ), g u

Scalar affine change of variables for the real endpoint estimates in blueprint lem:absolute, line 388.

theorem TrilinearHT.Auto.real_progression_pair_lintegral (f g : ℝ → ENNReal) (hf : Measurable f) (hg : Measurable g) {i j : ℝ} (hij : i ≠ j) : ∫⁻ (z : ℝ × ℝ), f (z.1 + i * z.2) * g (z.1 + j * z.2) = (ENNReal.ofReal |(j - i)⁻¹| * ∫⁻ (u : ℝ), f u) * ∫⁻ (v : ℝ), g v

The two occupied real progression slots have Jacobian j - i, as used by blueprint lem:absolute, line 388.

def TrilinearHT.Auto.realProgressionCoordinate (j : Fin 4) (z : ℝ × ℝ) : ℝ

The four real progression coordinates in blueprint eq:local.

Equations

• TrilinearHT.Auto.realProgressionCoordinate j z = z.1 + ↑↑j * z.2

theorem TrilinearHT.Auto.continuous_realProgressionCoordinate (j : Fin 4) : Continuous (realProgressionCoordinate j)

noncomputable def TrilinearHT.Auto.localProgressionForm (r : ℝ) (w : ℝ × ℝ → ℂ) (f : Fin 4 → ℝ → ℂ) : ℂ

Blueprint eq:local: the scale-normalized local complex form.

Equations

• TrilinearHT.Auto.localProgressionForm r w f = (↑r)⁻¹ ^ 2 * ∫ (z : ℝ × ℝ), w z * ∏ j : Fin 4, f j (TrilinearHT.Auto.realProgressionCoordinate j z)

def TrilinearHT.Auto.HasLocalProgressionSupport {E : Type u_1} [Zero E] (a r : ℝ) (w : ℝ × ℝ → E) : Prop

Interval support required of the kernel in blueprint eq:local. The stronger interior-support and smoothness conditions imply this condition.

Equations

• TrilinearHT.Auto.HasLocalProgressionSupport a r w = ∀ (z : ℝ × ℝ), w z ≠ 0 → ∀ (j : Fin 4), TrilinearHT.Auto.realProgressionCoordinate j z ∈ Set.Icc a (a + r)

theorem TrilinearHT.Auto.localProgressionSupport_time {E : Type u_1} [Zero E] {a r : ℝ} (hr : 0 ≤ r) {w : ℝ × ℝ → E} (hw : HasLocalProgressionSupport a r w) {z : ℝ × ℝ} (hz : w z ≠ 0) : z.2 ∈ Set.Icc (-r) r

The support of a local progression kernel has a scale-sized time fiber.

noncomputable def TrilinearHT.Auto.normalizedIntervalMeasure (a r : ℝ) : MeasureTheory.Measure ℝ

Normalized Lebesgue measure on a source interval, for the local Lp norms.

Equations

• TrilinearHT.Auto.normalizedIntervalMeasure a r = ENNReal.ofReal r⁻¹ • MeasureTheory.volume.restrict (Set.Icc a (a + r))

theorem TrilinearHT.Auto.normalizedIntervalMeasure_probability (a : ℝ) {r : ℝ} (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (normalizedIntervalMeasure a r)

theorem TrilinearHT.Auto.realProgression_pair_jacobian_le_one {i j : Fin 4} (hij : i ≠ j) : ENNReal.ofReal |(↑↑j - ↑↑i)⁻¹| ≤ 1

theorem TrilinearHT.Auto.localProgression_pair_endpoint {a r : ℝ} {K : ℝ × ℝ → ENNReal} (hK : HasLocalProgressionSupport a r K) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), K z ≤ W) (f g : ℝ → ENNReal) (hf : Measurable f) (hg : Measurable g) {i j : Fin 4} (hij : i ≠ j) : ∫⁻ (z : ℝ × ℝ), K z * (f (realProgressionCoordinate i z) * g (realProgressionCoordinate j z)) ≤ (W * ∫⁻ (u : ℝ) in Set.Icc a (a + r), f u) * ∫⁻ (v : ℝ) in Set.Icc a (a + r), g v

The two-L1 endpoint in blueprint lem:absolute, line 388.

theorem TrilinearHT.Auto.real_progression_time_cutoff_lintegral (F : ℝ → ENNReal) (hF : Measurable F) (r i : ℝ) : ∫⁻ (z : ℝ × ℝ), (Set.Icc (-r) r).indicator (fun (x : ℝ) => 1) z.2 * F (z.1 + i * z.2) = ENNReal.ofReal (2 * r) * ∫⁻ (u : ℝ), F u

theorem TrilinearHT.Auto.localProgression_single_endpoint {a r : ℝ} (hr : 0 ≤ r) {K : ℝ × ℝ → ENNReal} (hK : HasLocalProgressionSupport a r K) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), K z ≤ W) (f : ℝ → ENNReal) (hf : Measurable f) (i : Fin 4) : ∫⁻ (z : ℝ × ℝ), K z * f (realProgressionCoordinate i z) ≤ W * ENNReal.ofReal (2 * r) * ∫⁻ (u : ℝ) in Set.Icc a (a + r), f u

The one-L1 endpoint in blueprint lem:absolute, line 388.

theorem TrilinearHT.Auto.localProgression_empty_endpoint {a r : ℝ} (hr : 0 ≤ r) {K : ℝ × ℝ → ENNReal} (hK : HasLocalProgressionSupport a r K) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), K z ≤ W) : ∫⁻ (z : ℝ × ℝ), K z ≤ W * ENNReal.ofReal (2 * r) * ENNReal.ofReal r

The all-infinity endpoint in blueprint lem:absolute, line 388.

theorem TrilinearHT.Auto.measurePreserving_pair_endpoint {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {ρ : MeasureTheory.Measure Z} [MeasureTheory.SFinite ρ] {P : X → Y × Z} (hP : MeasureTheory.MeasurePreserving P μ (ν.prod ρ)) {K : X → ENNReal} {W : ENNReal} (hW : ∀ (x : X), K x ≤ W) (f : Y → ENNReal) (g : Z → ENNReal) (hf : Measurable f) (hg : Measurable g) : ∫⁻ (x : X), K x * (f (P x).1 * g (P x).2) ∂μ ≤ (W * ∫⁻ (y : Y), f y ∂ν) * ∫⁻ (z : Z), g z ∂ρ

A two-coordinate measure-preserving map supplies a positive endpoint bound, as in the torus argument of blueprint lem:absolute, line 394.

theorem TrilinearHT.Auto.rationalTorus_pair_endpoint {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) {K : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal} {W : ENNReal} (hW : ∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z ≤ W) (f g : ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal) (hf : Measurable f) (hg : Measurable g) {i j : ℤ} (hij : i ≠ j) (l : ℤ) : ∫⁻ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z * (f (z.1 + (i - l) • z.2) * g (z.1 + (j - l) • z.2)) ∂(torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V)) ≤ (W * ∫⁻ (u : ↥(torusAnnihilator (rationalIntegerIntersection V))), f u ∂torusAnnihilatorHaar (rationalIntegerIntersection V)) * ∫⁻ (v : ↥(torusAnnihilator (rationalIntegerIntersection V))), g v ∂torusAnnihilatorHaar (rationalIntegerIntersection V)

Blueprint lem:absolute, torus two-slot endpoint with constant one for a multiplier bounded by one.

theorem TrilinearHT.Auto.rationalTorus_single_endpoint {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) {K : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal} {W : ENNReal} (hW : ∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z ≤ W) (f : ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal) (hf : Measurable f) (i l : ℤ) : ∫⁻ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z * f (z.1 + (i - l) • z.2) ∂(torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V)) ≤ W * ∫⁻ (u : ↥(torusAnnihilator (rationalIntegerIntersection V))), f u ∂torusAnnihilatorHaar (rationalIntegerIntersection V)

theorem TrilinearHT.Auto.rationalTorus_empty_endpoint {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) {K : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal} {W : ENNReal} (hW : ∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z ≤ W) : ∫⁻ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z ∂(torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V)) ≤ W

theorem TrilinearHT.Auto.reciprocalExponentEndpoints_support {d k : ℕ} {a : Fin d → ℝ} (ha : a ∈ reciprocalExponentEndpoints d k) : ∃ (S : Finset (Fin d)), S.card ≤ k ∧ ∀ (i : Fin d), a i = if i ∈ S then 1 else 0

theorem TrilinearHT.Auto.positivePairwise_power_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) {d : ℕ} (P : Fin d → X → Y) (hP : ∀ (i : Fin d), Measurable (P i)) (C : ENNReal) (hempty : μ Set.univ ≤ C) (hsingle : ∀ (i : Fin d) (f : Y → ENNReal), Measurable f → ∫⁻ (x : X), f (P i x) ∂μ ≤ C * ∫⁻ (y : Y), f y ∂ν) (hpair : ∀ (i j : Fin d), i ≠ j → ∀ (f g : Y → ENNReal), Measurable f → Measurable g → ∫⁻ (x : X), f (P i x) * g (P j x) ∂μ ≤ (C * ∫⁻ (y : Y), f y ∂ν) * ∫⁻ (y : Y), g y ∂ν) (f : Fin d → Y → ENNReal) (hf : ∀ (i : Fin d), Measurable (f i)) {a : Fin d → ℝ} (ha : a ∈ reciprocalExponentPolytope d 2) : ∫⁻ (x : X), ∏ i : Fin d, f i (P i x) ^ a i ∂μ ≤ C * ∏ i : Fin d, (∫⁻ (y : Y), f i y ∂ν) ^ a i

Abstract positive rank-two estimate obtained from the empty, singleton and pair endpoints. This assembles the interpolation argument in lem:absolute.

theorem TrilinearHT.Auto.quasiMeasurePreserving_of_positive_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {P : X → Y} (hP : Measurable P) (C : ENNReal) (hbound : ∀ (f : Y → ENNReal), Measurable f → ∫⁻ (x : X), f (P x) ∂μ ≤ C * ∫⁻ (y : Y), f y ∂ν) : MeasureTheory.QuasiMeasurePreserving P μ ν

noncomputable def TrilinearHT.Auto.interpolationMoment {Y : Sort u_1} (p : ENNReal) (f : Y → ENNReal) : Y → ENNReal

The finite moment used for positive interpolation; an infinity slot contributes the constant one and is bounded by its essential supremum.

Equations

• TrilinearHT.Auto.interpolationMoment p f y = if p = ⊤ then 1 else f y ^ p.toReal

noncomputable def TrilinearHT.Auto.interpolationInfinityFactor {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) (p : ENNReal) (f : Y → ENNReal) : ENNReal

The essential-supremum factor used at the infinite interpolation endpoint.

Equations

• TrilinearHT.Auto.interpolationInfinityFactor ν p f = if p = ⊤ then MeasureTheory.eLpNorm f ⊤ ν else 1

theorem TrilinearHT.Auto.measurable_interpolationMoment {Y : Type u_1} [MeasurableSpace Y] {f : Y → ENNReal} (hf : Measurable f) (p : ENNReal) : Measurable (interpolationMoment p f)

theorem TrilinearHT.Auto.interpolationMoment_ae_bound {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) (f : Y → ENNReal) {p : ENNReal} (hp : 1 ≤ p) : ∀ᵐ (y : Y) ∂ν, f y ≤ interpolationInfinityFactor ν p f * interpolationMoment p f y ^ p.toReal⁻¹

theorem TrilinearHT.Auto.interpolationMoment_norm_identity {Y : Type u_1} [MeasurableSpace Y] (ν : MeasureTheory.Measure Y) {f : Y → ENNReal} (hf : Measurable f) {p : ENNReal} (hp : 1 ≤ p) : interpolationInfinityFactor ν p f * (∫⁻ (y : Y), interpolationMoment p f y ∂ν) ^ p.toReal⁻¹ = MeasureTheory.eLpNorm f p ν

theorem TrilinearHT.Auto.positivePairwise_eLpNorm_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) {d : ℕ} (P : Fin d → X → Y) (hP : ∀ (i : Fin d), Measurable (P i)) (C : ENNReal) (hempty : μ Set.univ ≤ C) (hsingle : ∀ (i : Fin d) (f : Y → ENNReal), Measurable f → ∫⁻ (x : X), f (P i x) ∂μ ≤ C * ∫⁻ (y : Y), f y ∂ν) (hpair : ∀ (i j : Fin d), i ≠ j → ∀ (f g : Y → ENNReal), Measurable f → Measurable g → ∫⁻ (x : X), f (P i x) * g (P j x) ∂μ ≤ (C * ∫⁻ (y : Y), f y ∂ν) * ∫⁻ (y : Y), g y ∂ν) (f : Fin d → Y → ENNReal) (hf : ∀ (i : Fin d), Measurable (f i)) (p : Fin d → ENNReal) (hp : ∀ (i : Fin d), 1 ≤ p i) (hsum : ∑ i : Fin d, (p i).toReal⁻¹ ≤ 2) : ∫⁻ (x : X), ∏ i : Fin d, f i (P i x) ∂μ ≤ C * ∏ i : Fin d, MeasureTheory.eLpNorm (f i) (p i) ν

The full Lp version of positive rank-two interpolation, including infinity exponents and zero or infinite norms, used in blueprint eq:absolute.

theorem TrilinearHT.Auto.positiveWeightedPairwise_eLpNorm_bound {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) {d : ℕ} (P : Fin d → X → Y) (hP : ∀ (i : Fin d), Measurable (P i)) (K : X → ENNReal) (hK : Measurable K) (C : ENNReal) (hempty : ∫⁻ (x : X), K x ∂μ ≤ C) (hsingle : ∀ (i : Fin d) (f : Y → ENNReal), Measurable f → ∫⁻ (x : X), K x * f (P i x) ∂μ ≤ C * ∫⁻ (y : Y), f y ∂ν) (hpair : ∀ (i j : Fin d), i ≠ j → ∀ (f g : Y → ENNReal), Measurable f → Measurable g → ∫⁻ (x : X), K x * (f (P i x) * g (P j x)) ∂μ ≤ (C * ∫⁻ (y : Y), f y ∂ν) * ∫⁻ (y : Y), g y ∂ν) (f : Fin d → Y → ENNReal) (hf : ∀ (i : Fin d), Measurable (f i)) (p : Fin d → ENNReal) (hp : ∀ (i : Fin d), 1 ≤ p i) (hsum : ∑ i : Fin d, (p i).toReal⁻¹ ≤ 2) : ∫⁻ (x : X), K x * ∏ i : Fin d, f i (P i x) ∂μ ≤ C * ∏ i : Fin d, MeasureTheory.eLpNorm (f i) (p i) ν

Weighted version of the positive rank-two estimate. The three hypotheses are precisely the endpoint integrals proved in the three source settings.

theorem TrilinearHT.Auto.rationalTorus_absoluteBound {d : ℕ} (V : Submodule ℚ (Fin d → ℚ)) (K : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal) (hK : Measurable K) {W : ENNReal} (hW : ∀ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z ≤ W) (l : ℤ) (f : Fin 4 → ↥(torusAnnihilator (rationalIntegerIntersection V)) → ENNReal) (hf : ∀ (i : Fin 4), Measurable (f i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) : ∫⁻ (z : ↥(torusAnnihilator (rationalIntegerIntersection V)) × ↥(torusAnnihilator (rationalIntegerIntersection V))), K z * ∏ i : Fin 4, f i (z.1 + (↑↑i - l) • z.2) ∂(torusAnnihilatorHaar (rationalIntegerIntersection V)).prod (torusAnnihilatorHaar (rationalIntegerIntersection V)) ≤ W * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (torusAnnihilatorHaar (rationalIntegerIntersection V))

Blueprint eq:absolute on every rational connected subtorus, with the exact multiplier constant and all exponents in [1, ∞].

theorem TrilinearHT.Auto.localProgression_absoluteBound {a r : ℝ} (hr : 0 < r) (K : ℝ × ℝ → ENNReal) (hK : Measurable K) (hsupport : HasLocalProgressionSupport a r K) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), K z ≤ W) (f : Fin 4 → ℝ → ENNReal) (hf : ∀ (i : Fin 4), Measurable (f i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) : ENNReal.ofReal r⁻¹ ^ 2 * ∫⁻ (z : ℝ × ℝ), K z * ∏ i : Fin 4, f i (realProgressionCoordinate i z) ≤ 2 * W * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (normalizedIntervalMeasure a r)

Blueprint eq:absolute on the real line: the normalized positive local form is bounded for every exponent in [1, ∞] with reciprocal sum at most two. Only boundedness and interval support of the kernel are needed.

theorem TrilinearHT.Auto.localProgression_absoluteNormBound {a r : ℝ} (hr : 0 < r) (w : ℝ × ℝ → ℂ) (hw : Measurable w) (hsupport : HasLocalProgressionSupport a r w) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), ‖w z‖ₑ ≤ W) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) : ENNReal.ofReal r⁻¹ ^ 2 * ∫⁻ (z : ℝ × ℝ), ‖w z‖ₑ * ∏ i : Fin 4, ‖f i (realProgressionCoordinate i z)‖ₑ ≤ 2 * W * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (normalizedIntervalMeasure a r)

Blueprint eq:absolute for the actual complex local kernel and inputs. The nonnegative integral gives the intended interpretation even for infinite norms.

theorem TrilinearHT.Auto.localProgressionForm_enorm_le {a r : ℝ} (hr : 0 < r) (w : ℝ × ℝ → ℂ) (hw : Measurable w) (hsupport : HasLocalProgressionSupport a r w) {W : ENNReal} (hW : ∀ (z : ℝ × ℝ), ‖w z‖ₑ ≤ W) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) (p : Fin 4 → ENNReal) (hp : ∀ (i : Fin 4), 1 ≤ p i) (hsum : ∑ i : Fin 4, (p i).toReal⁻¹ ≤ 2) : ‖localProgressionForm r w f‖ₑ ≤ 2 * W * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (p i) (normalizedIntervalMeasure a r)

The complex local form is controlled by the positive local estimate. This is the form of lem:absolute used in lem:finite-CN.

structure TrilinearHT.Auto.LocalKernelClass : Type

Fixed constants defining the admissible kernel class, blueprint line 371.

• margin : ℝ

  Positive margin in the admissible local-kernel estimates.

• margin_pos : 0 < self.margin
• derivativeConstant : ℝ

  Constant controlling all orders of local-kernel derivatives.

• one_le_derivativeConstant : 1 ≤ self.derivativeConstant

noncomputable def TrilinearHT.Auto.localKernelPartial (m n : ℕ) (w : ℝ × ℝ → ℂ) (z : ℝ × ℝ) : ℂ

Coordinate partial derivative of a local kernel. This keeps the source's total-order derivative convention rather than replacing it by an operator norm.

Equations

• TrilinearHT.Auto.localKernelPartial m n w z = iteratedDeriv m (fun (x : ℝ) => iteratedDeriv n (fun (t : ℝ) => w (x, t)) z.2) z.1

structure TrilinearHT.Auto.IsAdmissibleLocalKernel (κ : LocalKernelClass) (a r : ℝ) (w : ℝ × ℝ → ℂ) : Prop

Smoothness, interior support, four zero marginals, and the quantitative derivative bounds in blueprint eq:local and eq:marginals, lines 371–376.

• smooth : ContDiff ℝ (↑⊤) w
• support (z : ℝ × ℝ) : w z ≠ 0 → ∀ (j : Fin 4), a + κ.margin * r ≤ realProgressionCoordinate j z ∧ realProgressionCoordinate j z ≤ a + r - κ.margin * r
• marginal (u : ℝ) (j : Fin 4) : ∫ (t : ℝ), w (u - ↑↑j * t, t) = 0
• derivativeBound (m n : ℕ) (z : ℝ × ℝ) : ‖localKernelPartial m n w z‖ ≤ r⁻¹ ^ (m + n) * (κ.derivativeConstant * (↑(m + n) + 2)) ^ (κ.derivativeConstant * (↑(m + n) + 2))

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

Uniform pointwise bound supplied by the zeroth-order kernel estimate.

Equations

• TrilinearHT.Auto.localKernelSupBound κ = (κ.derivativeConstant * 2) ^ (κ.derivativeConstant * 2)

theorem TrilinearHT.Auto.localKernelSupBound_nonneg (κ : LocalKernelClass) : 0 ≤ localKernelSupBound κ

theorem TrilinearHT.Auto.admissibleLocalKernel_norm_le {κ : LocalKernelClass} {a r : ℝ} {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) (z : ℝ × ℝ) : ‖w z‖ ≤ localKernelSupBound κ

theorem TrilinearHT.Auto.admissibleLocalKernel_support {κ : LocalKernelClass} {a r : ℝ} (hr : 0 ≤ r) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) : HasLocalProgressionSupport a r w

noncomputable def TrilinearHT.Auto.scalarMaximalQ (q : ℝ) (f : ℝ → ℂ) (x : ℝ) : ENNReal

The scalar specialization of the source's uncentered powered maximal function.

Equations

• TrilinearHT.Auto.scalarMaximalQ q f x = TrilinearHT.Auto.maximalQ q (fun (z : ℝ × Unit) => f z.1) (x, ())

structure TrilinearHT.Auto.FiniteDepthLocalData (κ : LocalKernelClass) (q : ℝ) (N : ℕ) : Type

The complete finite data quantified over by blueprint eq:CN: one dyadic grid, a finite collection in at most N consecutive depths, an admissible kernel at every selected cell, and compactly supported measurable Lq inputs.

• grid : RealDyadicGrid

  Dyadic grid supporting the finite-depth local form.

• cells : Finset (ℤ × ℤ)

  Finite collection of dyadic cells used in the local form.

• firstDepth : ℤ

  First permitted depth in the finite-depth window.

• depths (c : ℤ × ℤ) : c ∈ self.cells → self.firstDepth ≤ c.1 ∧ c.1 < self.firstDepth + ↑N
• kernel : ℤ × ℤ → ℝ × ℝ → ℂ

  Local kernel assigned to each dyadic cell.

• admissible (c : ℤ × ℤ) : c ∈ self.cells → IsAdmissibleLocalKernel κ (dyadicGridLeft self.grid c.1 c.2) (dyadicGridLength self.grid c.1) (self.kernel c)
• input : Fin 4 → ℝ → ℂ

  The four measurable, compactly supported inputs to the local form.

• measurable_input (i : Fin 4) : Measurable (self.input i)
• memLp_input (i : Fin 4) : MeasureTheory.MemLp (self.input i) (ENNReal.ofReal q) MeasureTheory.volume
• compact_input (i : Fin 4) : HasCompactSupport (self.input i)

noncomputable def TrilinearHT.Auto.finiteDepthNumerator {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) : ℝ

The finite numerator in blueprint eq:CN.

Equations

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

noncomputable def TrilinearHT.Auto.finiteDepthDenominator {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) : ENNReal

The nonnegative maximal-product denominator in blueprint eq:CN.

Equations

• TrilinearHT.Auto.finiteDepthDenominator D = ∫⁻ (x : ℝ), ∏ i : Fin 4, TrilinearHT.Auto.scalarMaximalQ q (D.input i) x

def TrilinearHT.Auto.finiteDepthRatios (κ : LocalKernelClass) (q : ℝ) (N : ℕ) : Set ℝ

Only strictly positive finite denominators enter the real ratios in blueprint eq:CN, lines 398–403.

Equations

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

noncomputable def TrilinearHT.Auto.finiteDepthConstant (κ : LocalKernelClass) (q : ℝ) (N : ℕ) : ℝ

The least constant at least one from blueprint eq:CN. Inserting one before the supremum includes the empty-ratio case without a division convention.

Equations

• TrilinearHT.Auto.finiteDepthConstant κ q N = sSup (insert 1 (TrilinearHT.Auto.finiteDepthRatios κ q N))

theorem TrilinearHT.Auto.finiteDepthNumerator_nonneg {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) : 0 ≤ finiteDepthNumerator D

theorem TrilinearHT.Auto.localLpNorm_le_scalarMaximalQ {a r x q : ℝ} (hr : 0 < r) (hq : 0 < q) (hx : x ∈ Set.Icc a (a + r)) (f : ℝ → ℂ) (hf : Measurable f) : MeasureTheory.eLpNorm f (ENNReal.ofReal q) (normalizedIntervalMeasure a r) ≤ scalarMaximalQ q f x

Every normalized local Lq norm is bounded by the source's uncentered M_q at every point of the interval, as used in lem:finite-CN, line 409.

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

The uniform real constant furnished by the fixed admissible kernel class.

Equations

• TrilinearHT.Auto.localFormUniformConstant κ = 2 * TrilinearHT.Auto.localKernelSupBound κ

theorem TrilinearHT.Auto.localFormUniformConstant_nonneg (κ : LocalKernelClass) : 0 ≤ localFormUniformConstant κ

theorem TrilinearHT.Auto.admissibleLocalForm_le_localLp {κ : LocalKernelClass} {a r q : ℝ} (hr : 0 < r) (hq : 2 ≤ q) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) : ‖localProgressionForm r w f‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * ∏ i : Fin 4, MeasureTheory.eLpNorm (f i) (ENNReal.ofReal q) (normalizedIntervalMeasure a r)

The local L2 estimate followed by normalized exponent monotonicity, the first step of blueprint lem:finite-CN, line 409.

theorem TrilinearHT.Auto.admissibleLocalForm_le_maximalProduct {κ : LocalKernelClass} {a r q x : ℝ} (hr : 0 < r) (hq : 2 ≤ q) (hx : x ∈ Set.Icc a (a + r)) {w : ℝ × ℝ → ℂ} (hw : IsAdmissibleLocalKernel κ a r w) (f : Fin 4 → ℝ → ℂ) (hf : ∀ (i : Fin 4), Measurable (f i)) : ‖localProgressionForm r w f‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * ∏ i : Fin 4, scalarMaximalQ q (f i) x

The source local form is bounded pointwise on its interval by the product of the four uncentered maximal functions.

theorem TrilinearHT.Auto.finiteDepth_cell_bound {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (hq : 2 ≤ q) {c : ℤ × ℤ} (hc : c ∈ D.cells) : ENNReal.ofReal (dyadicGridLength D.grid c.1) * ‖localProgressionForm (dyadicGridLength D.grid c.1) (D.kernel c) D.input‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * ∫⁻ (x : ℝ) in dyadicGridCell D.grid c.1 c.2, ∏ i : Fin 4, scalarMaximalQ q (D.input i) x

theorem TrilinearHT.Auto.finiteDepth_one_level_bound {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (hq : 2 ≤ q) (s : ℤ) : ∑ c ∈ D.cells with c.1 = s, ENNReal.ofReal (dyadicGridLength D.grid c.1) * ‖localProgressionForm (dyadicGridLength D.grid c.1) (D.kernel c) D.input‖ₑ ≤ ENNReal.ofReal (localFormUniformConstant κ) * finiteDepthDenominator D

theorem TrilinearHT.Auto.finiteDepthNumerator_ofReal {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) : ENNReal.ofReal (finiteDepthNumerator D) = ∑ c ∈ D.cells, ENNReal.ofReal (dyadicGridLength D.grid c.1) * ‖localProgressionForm (dyadicGridLength D.grid c.1) (D.kernel c) D.input‖ₑ

theorem TrilinearHT.Auto.finiteDepthNumerator_le {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (hq : 2 ≤ q) : ENNReal.ofReal (finiteDepthNumerator D) ≤ ENNReal.ofReal (localFormUniformConstant κ * ↑N) * finiteDepthDenominator D

Blueprint lem:finite-CN, line 409: disjoint depth summation gives the uniform linear-in-depth bound before the absorption argument begins.

theorem TrilinearHT.Auto.finiteDepth_ratio_le {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (D : FiniteDepthLocalData κ q N) (hq : 2 ≤ q) (hpos : 0 < finiteDepthDenominator D) (hfin : finiteDepthDenominator D ≠ ⊤) : finiteDepthNumerator D / (finiteDepthDenominator D).toReal ≤ localFormUniformConstant κ * ↑N

theorem TrilinearHT.Auto.finiteDepthRatios_bddAbove (κ : LocalKernelClass) {q : ℝ} (hq : 2 ≤ q) (N : ℕ) : BddAbove (insert 1 (finiteDepthRatios κ q N))

theorem TrilinearHT.Auto.finiteDepthConstant_bounds (κ : LocalKernelClass) {q : ℝ} (hq : 2 ≤ q) (N : ℕ) : 1 ≤ finiteDepthConstant κ q N ∧ finiteDepthConstant κ q N ≤ 1 + localFormUniformConstant κ * ↑N

Blueprint eq:CN and lem:finite-CN: the real supremum is bounded, and the inserted value one enforces the required normalization.

theorem TrilinearHT.Auto.finiteDepthConstant_spec {κ : LocalKernelClass} {q : ℝ} {N : ℕ} (hq : 2 ≤ q) (D : FiniteDepthLocalData κ q N) : ENNReal.ofReal (finiteDepthNumerator D) ≤ ENNReal.ofReal (finiteDepthConstant κ q N) * finiteDepthDenominator D

Blueprint eq:CN: the defining inequality holds at the real supremum, including zero and infinite denominator cases.

theorem TrilinearHT.Auto.finiteDepthConstant_least {κ : LocalKernelClass} {q : ℝ} {N : ℕ} {c : ℝ} (hc : 1 ≤ c) (hbound : ∀ (D : FiniteDepthLocalData κ q N), ENNReal.ofReal (finiteDepthNumerator D) ≤ ENNReal.ofReal c * finiteDepthDenominator D) : finiteDepthConstant κ q N ≤ c

Blueprint eq:CN: every admissible real constant at least one majorizes the constructed constant.