Section 8: Continuous witnesses and a bounded decomposition

This file was automatically generated by Claude.

Formalization of blueprint Section 8, "Continuous witnesses and a bounded decomposition" (sec:continuous, lines 1164-1243) of blueprint/formalization_blueprint.tex.

theorem TrilinearHT.Auto.l2CubeContinuous_toLp {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : (Fin 3 → Bool) → G → ℂ) (hf : ∀ (ω : Fin 3 → Bool), Measurable (f ω)) (hfl : ∀ (ω : Fin 3 → Bool), MeasureTheory.MemLp (f ω) 2 μ) : ((l2CubeContinuous μ) fun (ω : Fin 3 → Bool) => MeasureTheory.MemLp.toLp (f ω) ⋯) = cubeAverage μ 3 f

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

theorem TrilinearHT.Auto.exists_cyclic_cell_large_gowersNorm (g : ℝ → ℂ) (hg : Measurable g) (hunit : ∀ (x : ℝ), ‖g x‖ ≤ 1) (hsupp : ∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Icc 0 1) {δ : ℝ} (hδ : 0 < δ) (hnorm : δ ≤ gowersNorm AddCircle.haarAddCircle 3 (AddCircle.liftIoc 16 (-8) g)) : ∃ (L : ℕ), 0 < L ∧ δ / 2 ≤ gowersNorm (finiteHaar (ZMod (16 * L + 1))) 3 (cyclicCellAverage L g)

theorem TrilinearHT.Auto.cyclicCellAverage_correlation_eq (L : ℕ) (g : ℝ → ℂ) (b : ℕ → ℂ) : (Finset.univ.expect fun (x : ZMod (16 * L + 1)) => cyclicCellAverage L g x * b x.val) = ↑L / (16 * ↑L + 1) * ∑ k ∈ Finset.range L, (∫ (x : ℝ) in ↑k / ↑L..(↑k + 1) / ↑L, g x) * b k

theorem TrilinearHT.Auto.cyclicCellAverage_correlation_le_cell_sum (L : ℕ) (g : ℝ → ℂ) (b : ℕ → ℂ) : ‖Finset.univ.expect fun (x : ZMod (16 * L + 1)) => cyclicCellAverage L g x * b x.val‖ ≤ ‖∑ k ∈ Finset.range L, (∫ (x : ℝ) in ↑k / ↑L..(↑k + 1) / ↑L, g x) * b k‖

theorem TrilinearHT.Auto.floor_on_unit_cell {L : ℕ} (hL : 0 < L) (k : ℕ) {x : ℝ} (hx : x ∈ Set.Ioo (↑k / ↑L) ((↑k + 1) / ↑L)) : ⌊↑L * x⌋ = ↑k

theorem TrilinearHT.Auto.cell_sum_eq_floor_integral {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hg : Measurable g) (hgb : ∀ (x : ℝ), ‖g x‖ ≤ 1) (b : ℤ → ℂ) (hbb : ∀ (n : ℤ), ‖b n‖ ≤ 1) : ∑ k ∈ Finset.range L, (∫ (x : ℝ) in ↑k / ↑L..(↑k + 1) / ↑L, g x) * b ↑k = ∫ (x : ℝ) in 0..1, g x * b ⌊↑L * x⌋

theorem TrilinearHT.Auto.bounded_measurable_real_intervalIntegrable (f : ℝ → ℝ) (hf : Measurable f) {M : ℝ} (hb : ∀ (x : ℝ), |f x| ≤ M) (a b : ℝ) : IntervalIntegrable f MeasureTheory.volume a b

theorem TrilinearHT.Auto.integral_fract_nat_mul {L : ℕ} (hL : 0 < L) (f : ℝ → ℝ) (hf : Measurable f) {M : ℝ} (hb : ∀ (x : ℝ), |f x| ≤ M) : ∫ (x : ℝ) in 0..1, f (Int.fract (↑L * x)) = ∫ (x : ℝ) in 0..1, f x

theorem TrilinearHT.Auto.endpoint_cutoff_integral_error (η : ℝ → ℝ) (hη : Continuous η) (hunit : ∀ (x : ℝ), η x ∈ Set.Icc 0 1) {ε : ℝ} (hε : 0 ≤ ε) (hεh : ε ≤ 1 / 2) (hone : ∀ x ∈ Set.Icc ε (1 - ε), η x = 1) : ∫ (x : ℝ) in 0..1, 1 - η x ≤ 2 * ε

theorem TrilinearHT.Auto.floor_cutoff_correlation_error {L : ℕ} (hL : 0 < L) (g : ℝ → ℂ) (hg : Measurable g) (hgb : ∀ (x : ℝ), ‖g x‖ ≤ 1) (b : ℤ → ℂ) (hbb : ∀ (n : ℤ), ‖b n‖ ≤ 1) (η : ℝ → ℝ) (hη : Continuous η) (hunit : ∀ (x : ℝ), η x ∈ Set.Icc 0 1) {ε : ℝ} (hε : 0 ≤ ε) (hεh : ε ≤ 1 / 2) (hone : ∀ x ∈ Set.Icc ε (1 - ε), η x = 1) : ‖(∫ (x : ℝ) in 0..1, g x * b ⌊↑L * x⌋) - ∫ (x : ℝ) in 0..1, ↑(η (Int.fract (↑L * x))) * (g x * b ⌊↑L * x⌋)‖ ≤ 2 * ε

noncomputable def TrilinearHT.Auto.normalizeIntervalFunction (a b : ℝ) (f : ℝ → ℂ) : ℝ → ℂ

Pull an interval function back to [0,1) and extend it by zero.

Equations

• TrilinearHT.Auto.normalizeIntervalFunction a b f = (Set.Ico 0 1).indicator fun (x : ℝ) => f (a + (b - a) * x)

theorem TrilinearHT.Auto.normalizeIntervalFunction_measurable (a b : ℝ) (f : ℝ → ℂ) (hf : Measurable f) : Measurable (normalizeIntervalFunction a b f)

theorem TrilinearHT.Auto.normalizeIntervalFunction_support (a b : ℝ) (f : ℝ → ℂ) (x : ℝ) (hx : normalizeIntervalFunction a b f x ≠ 0) : x ∈ Set.Ico 0 1

theorem TrilinearHT.Auto.normalizeIntervalFunction_norm_le_one {a b : ℝ} (hab : a < b) (f : ℝ → ℂ) (hf : ∀ x ∈ Set.Ico a b, ‖f x‖ ≤ 1) (x : ℝ) : ‖normalizeIntervalFunction a b f x‖ ≤ 1

noncomputable def TrilinearHT.Auto.intervalGowersNorm (a b : ℝ) (f : ℝ → ℂ) : ℝ

The interval uniformity norm: affine pullback to [0,1), zero extension to the torus of length 16, and probability-Haar U3.

Equations

• TrilinearHT.Auto.intervalGowersNorm a b f = TrilinearHT.Auto.gowersNorm AddCircle.haarAddCircle 3 (AddCircle.liftIoc 16 (-8) (TrilinearHT.Auto.normalizeIntervalFunction a b f))

theorem TrilinearHT.Auto.normalizeIntervalFunction_correlation {a b : ℝ} (hab : a < b) (f φ : ℝ → ℂ) : ∫ (y : ℝ) in 0..1, normalizeIntervalFunction a b f y * (starRingEnd ℂ) (φ (a + (b - a) * y)) = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x * (starRingEnd ℂ) (φ x)

noncomputable def TrilinearHT.Auto.l2GowersThreeNorm {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : ℝ

Third Gowers norm on L² obtained from the continuous eight-vertex cube form.

Equations

• TrilinearHT.Auto.l2GowersThreeNorm μ f = ((TrilinearHT.Auto.l2CubeContinuous μ) fun (x : Fin 3 → Bool) => f).re ^ 8⁻¹

theorem TrilinearHT.Auto.l2GowersThreeNorm_continuous {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : Continuous (l2GowersThreeNorm μ)

theorem TrilinearHT.Auto.l2GowersThreeNorm_toLp {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f : G → ℂ) (hf : Measurable f) (hfl : MeasureTheory.MemLp f 2 μ) : l2GowersThreeNorm μ (MeasureTheory.MemLp.toLp f hfl) = gowersNorm μ 3 f

theorem TrilinearHT.Auto.l2_simpleFunc_bounded_representative {G : Type u_1} [MeasurableSpace G] (μ : MeasureTheory.Measure G) (f : ↥(MeasureTheory.Lp.simpleFunc ℂ 2 μ)) : ∃ (g : G → ℂ) (_ : Measurable g) (hgl : MeasureTheory.MemLp g 2 μ), MeasureTheory.MemLp.toLp g hgl = ↑f ∧ ∃ (M : ℝ), ∀ (x : G), ‖g x‖ ≤ M

theorem TrilinearHT.Auto.l2GowersThreeNorm_add_le {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (f g : ↥(MeasureTheory.Lp ℂ 2 μ)) : l2GowersThreeNorm μ (f + g) ≤ l2GowersThreeNorm μ f + l2GowersThreeNorm μ g

theorem TrilinearHT.Auto.l2GowersThreeNorm_smul {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : l2GowersThreeNorm μ (c • f) = ‖c‖ * l2GowersThreeNorm μ f

noncomputable def TrilinearHT.Auto.l2GowersThreeSeminorm {G : Type u_1} [AddCommGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsAddLeftInvariant] [μ.IsNegInvariant] : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 μ)

The third Gowers norm packaged as a complex seminorm on L².

Equations

• TrilinearHT.Auto.l2GowersThreeSeminorm μ = Seminorm.of (TrilinearHT.Auto.l2GowersThreeNorm μ) ⋯ ⋯

The interval-to-torus L² realization used by lem:inverse, line 1218.

noncomputable def TrilinearHT.Auto.unitIntervalMeasure : MeasureTheory.Measure ℝ

Lebesgue measure restricted to the half-open unit interval.

Equations

• TrilinearHT.Auto.unitIntervalMeasure = MeasureTheory.volume.restrict (Set.Ico 0 1)

instance TrilinearHT.Auto.unitIntervalMeasure_probability : MeasureTheory.IsProbabilityMeasure unitIntervalMeasure

noncomputable def TrilinearHT.Auto.unitIntervalL2Extension (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : ℝ → ℂ

Chosen representative of a unit-interval L² class extended by zero.

Equations

• TrilinearHT.Auto.unitIntervalL2Extension f = (Set.Ico 0 1).indicator (TrilinearHT.Auto.l2Representative TrilinearHT.Auto.unitIntervalMeasure f)

theorem TrilinearHT.Auto.unitIntervalL2Extension_memLp (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : MeasureTheory.MemLp (unitIntervalL2Extension f) 2 MeasureTheory.volume

theorem TrilinearHT.Auto.circle_lift_ae_congr {f g : ℝ → ℂ} (hfg : f =ᵐ[MeasureTheory.volume] g) : AddCircle.liftIoc 16 (-8) f =ᵐ[AddCircle.haarAddCircle] AddCircle.liftIoc 16 (-8) g

theorem TrilinearHT.Auto.unitIntervalL2Circle_memLp (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : MeasureTheory.MemLp (AddCircle.liftIoc 16 (-8) (unitIntervalL2Extension f)) 2 AddCircle.haarAddCircle

noncomputable def TrilinearHT.Auto.unitIntervalL2Circle (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

Embed a unit-interval L² class in the circle of length sixteen.

Equations

• TrilinearHT.Auto.unitIntervalL2Circle f = MeasureTheory.MemLp.toLp (AddCircle.liftIoc 16 (-8) (TrilinearHT.Auto.unitIntervalL2Extension f)) ⋯

theorem TrilinearHT.Auto.unitIntervalL2Extension_add (f g : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : unitIntervalL2Extension (f + g) =ᵐ[MeasureTheory.volume] unitIntervalL2Extension f + unitIntervalL2Extension g

theorem TrilinearHT.Auto.unitIntervalL2Extension_smul (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : unitIntervalL2Extension (c • f) =ᵐ[MeasureTheory.volume] c • unitIntervalL2Extension f

theorem TrilinearHT.Auto.unitIntervalL2Circle_add (f g : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : unitIntervalL2Circle (f + g) = unitIntervalL2Circle f + unitIntervalL2Circle g

theorem TrilinearHT.Auto.unitIntervalL2Circle_smul (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : unitIntervalL2Circle (c • f) = c • unitIntervalL2Circle f

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

Linear embedding of unit-interval L² classes into the circle L² space.

Equations

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

theorem TrilinearHT.Auto.norm_toLp_sq_integral {X : Type u_1} [MeasurableSpace X] (ν : MeasureTheory.Measure X) (f : X → ℂ) (hf : MeasureTheory.MemLp f 2 ν) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (x : X), ‖f x‖ ^ 2 ∂ν

theorem TrilinearHT.Auto.unitIntervalL2Circle_norm_sq (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : ‖unitIntervalL2Circle f‖ ^ 2 = 1 / 16 * ‖f‖ ^ 2

theorem TrilinearHT.Auto.unitIntervalL2Circle_norm_le (f : ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)) : ‖unitIntervalL2Circle f‖ ≤ ‖f‖

noncomputable def TrilinearHT.Auto.unitIntervalGowersSeminorm : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)

Gowers seminorm on the unit interval induced by its circle embedding.

Equations

• TrilinearHT.Auto.unitIntervalGowersSeminorm = (TrilinearHT.Auto.l2GowersThreeSeminorm AddCircle.haarAddCircle).comp TrilinearHT.Auto.unitIntervalL2CircleLinear

theorem TrilinearHT.Auto.unitIntervalL2Extension_toLp {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 unitIntervalMeasure) : unitIntervalL2Extension (MeasureTheory.MemLp.toLp f hf) =ᵐ[MeasureTheory.volume] (Set.Ico 0 1).indicator f

theorem TrilinearHT.Auto.unitIntervalGowersSeminorm_toLp {f : ℝ → ℂ} (hf : Measurable f) (hfl : MeasureTheory.MemLp f 2 unitIntervalMeasure) : unitIntervalGowersSeminorm (MeasureTheory.MemLp.toLp f hfl) = intervalGowersNorm 0 1 f

theorem TrilinearHT.Auto.l2_bounded_measurable_representative {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) (hf : ∀ᵐ (x : X) ∂μ, ‖↑↑f x‖ ≤ 1) : ∃ (g : X → ℂ), Measurable g ∧ (∀ (x : X), ‖g x‖ ≤ 1) ∧ g =ᵐ[μ] ↑↑f

noncomputable def TrilinearHT.Auto.intervalProbabilityMeasure (a b : ℝ) : MeasureTheory.Measure ℝ

Probability measure obtained by the affine image of the unit interval.

Equations

• TrilinearHT.Auto.intervalProbabilityMeasure a b = MeasureTheory.Measure.map (fun (y : ℝ) => a + (b - a) * y) TrilinearHT.Auto.unitIntervalMeasure

theorem TrilinearHT.Auto.intervalAffine_measurePreserving (a b : ℝ) : MeasureTheory.MeasurePreserving (fun (y : ℝ) => a + (b - a) * y) unitIntervalMeasure (intervalProbabilityMeasure a b)

instance TrilinearHT.Auto.intervalProbabilityMeasure_probability (a b : ℝ) : MeasureTheory.IsProbabilityMeasure (intervalProbabilityMeasure a b)

noncomputable def TrilinearHT.Auto.intervalL2Pullback (a b : ℝ) : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure a b)) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 unitIntervalMeasure)

Isometric L² pullback along the affine parametrization of an interval.

Equations

• TrilinearHT.Auto.intervalL2Pullback a b = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℂ (fun (y : ℝ) => a + (b - a) * y) ⋯

noncomputable def TrilinearHT.Auto.intervalL2GowersSeminorm (a b : ℝ) : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure a b))

Interval Gowers seminorm obtained by affine pullback to the unit interval.

Equations

• TrilinearHT.Auto.intervalL2GowersSeminorm a b = TrilinearHT.Auto.unitIntervalGowersSeminorm.comp (TrilinearHT.Auto.intervalL2Pullback a b).toLinearMap

theorem TrilinearHT.Auto.intervalL2GowersSeminorm_toLp (a b : ℝ) {f : ℝ → ℂ} (hf : Measurable f) (hfl : MeasureTheory.MemLp f 2 (intervalProbabilityMeasure a b)) : (intervalL2GowersSeminorm a b) (MeasureTheory.MemLp.toLp f hfl) = intervalGowersNorm a b f

theorem TrilinearHT.Auto.intervalProbabilityMeasure_eq {a b : ℝ} (hab : a < b) : intervalProbabilityMeasure a b = ENNReal.ofReal (b - a)⁻¹ • MeasureTheory.volume.restrict (Set.Ico a b)

theorem TrilinearHT.Auto.integral_intervalProbabilityMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a < b) (f : ℝ → E) : ∫ (x : ℝ), f x ∂intervalProbabilityMeasure a b = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x

theorem TrilinearHT.Auto.intervalL2_inner_correlation {a b : ℝ} (hab : a < b) {f φ : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 (intervalProbabilityMeasure a b)) (hφ : MeasureTheory.MemLp φ 2 (intervalProbabilityMeasure a b)) : ‖inner ℂ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp φ hφ)‖ = (b - a)⁻¹ * ‖∫ (x : ℝ) in a..b, f x * (starRingEnd ℂ) (φ x)‖

theorem TrilinearHT.Auto.quadraticChartLatticeSummand_summable {d : ℕ} (A : QuadraticChartData d) (y : ℝ) : Summable (quadraticChartLatticeSummand A y)

theorem TrilinearHT.Auto.inverse_half_parameter_budget (C : ℕ) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ (δ : ℝ), 0 < δ → δ < 1 → Real.exp (↑C * (1 + Real.log (2 / δ)) ^ C) ≤ Real.exp (↑D * (1 + Real.log (1 / δ)) ^ D)

noncomputable def TrilinearHT.Auto.fractionalPhaseQuadraticChart {d : ℕ} (A : QuadraticChartData d) : QuadraticChartData d

Chart with its scalar quadratic and linear coefficients replaced by fractional parts.

Equations

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

theorem TrilinearHT.Auto.fractionalPhaseQuadraticChart_atom_int {d : ℕ} (A : QuadraticChartData d) (n : ℤ) : quadraticChartAtom (fractionalPhaseQuadraticChart A) ↑n = quadraticChartAtom A ↑n

theorem TrilinearHT.Auto.fractionalPhaseQuadraticChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : QuadraticChartComplexity c₀ H (fractionalPhaseQuadraticChart A)

theorem TrilinearHT.Auto.chart_horizontal_integer_reduction {d : ℕ} {H : ℝ} (hH : 0 ≤ H) (C : Matrix (Fin d) (Fin d) ℚ) (hC : ∀ (i j : Fin d), ↑(chartRationalHeight (C i j)) ≤ H) (v : Fin d → ℝ) : ∃ (P : ℕ) (m : Fin d → ℤ) (a : Fin d → ℝ), 0 < P ∧ ↑P ≤ H ^ d ^ 2 ∧ (∀ (i : Fin d), v i = ↑(m i) + a i) ∧ (∀ (i : Fin d), a i ∈ Set.Ico 0 ↑P) ∧ ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(C i j)

noncomputable def TrilinearHT.Auto.integerHorizontalQuadraticChart {d : ℕ} (A : QuadraticChartData d) (m : Fin d → ℤ) (a : Fin d → ℝ) : QuadraticChartData d

Chart after separating an integer part from its horizontal direction.

Equations

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

theorem TrilinearHT.Auto.integerHorizontalQuadraticChart_phased_summand {d : ℕ} (A : QuadraticChartData d) (m : Fin d → ℤ) (a : Fin d → ℝ) (hoff : ∀ (i : Fin d), A.horizontal i = ↑(m i) + a i) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(A.matrix i j)) (n : ℤ) (k : Fin d → ℤ) : ↑(Real.fourierChar ((integerHorizontalQuadraticChart A m a).quadratic * ↑n ^ 2 + (integerHorizontalQuadraticChart A m a).linear * ↑n)) * quadraticChartLatticeSummand (integerHorizontalQuadraticChart A m a) (↑n) k = ↑(Real.fourierChar (A.quadratic * ↑n ^ 2 + A.linear * ↑n)) * quadraticChartLatticeSummand A (↑n) (k + fun (i : Fin d) => m i * n)

theorem TrilinearHT.Auto.integerHorizontalQuadraticChart_atom_int {d : ℕ} (A : QuadraticChartData d) (m : Fin d → ℤ) (a : Fin d → ℝ) (hoff : ∀ (i : Fin d), A.horizontal i = ↑(m i) + a i) (hint : ∀ (i j : Fin d), ∃ (z : ℤ), ↑z = ↑(m i) * ↑(A.matrix i j)) (n : ℤ) : quadraticChartAtom (integerHorizontalQuadraticChart A m a) ↑n = quadraticChartAtom A ↑n

theorem TrilinearHT.Auto.integerHorizontalQuadraticChart_complexity {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (m : Fin d → ℤ) (a : Fin d → ℝ) : QuadraticChartComplexity c₀ H (integerHorizontalQuadraticChart A m a)

theorem TrilinearHT.Auto.quadraticChart_reduce_integer_parameters {d c₀ : ℕ} {H : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) : ∃ (P : ℕ) (B : QuadraticChartData d), 0 < P ∧ ↑P ≤ H ^ d ^ 2 ∧ QuadraticChartComplexity c₀ H B ∧ B.quadratic ∈ Set.Ico 0 1 ∧ B.linear ∈ Set.Ico 0 1 ∧ (∀ (i : Fin d), B.horizontal i ∈ Set.Ico 0 ↑P) ∧ B.matrix = A.matrix ∧ B.amplitude = A.amplitude ∧ ∀ (n : ℤ), quadraticChartAtom B ↑n = quadraticChartAtom A ↑n

Blueprint lem:inverse, line 1197: reduce all unrestricted real parameters at integer samples, without changing the rational matrix, cutoff, or complexity. The reduced chart need only retain the original atom's integer values.

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

Phase increment controlling the extra coordinate in floor interpolation.

Equations

• TrilinearHT.Auto.floorChartAlpha A = 2 * A.quadratic + TrilinearHT.Auto.chartMatrixPhase A.matrix A.horizontal A.horizontal

def TrilinearHT.Auto.floorChartTailMatrix : Matrix (Fin 2) (Fin 2) ℚ

Two-coordinate rational matrix encoding the floor-interpolation cross term.

Equations

• TrilinearHT.Auto.floorChartTailMatrix i j = if i = 1 ∧ j = 0 then -1 else 0

noncomputable def TrilinearHT.Auto.floorChartAmplitude {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (z : Fin (d + 2) → ℝ) : ℂ

Amplitude on the original coordinates and two added floor-interpolation coordinates.

Equations

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

theorem TrilinearHT.Auto.floorChartAmplitude_smooth {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hη : ContDiff ℝ (↑⊤) η) (hρ : ContDiff ℝ (↑⊤) ρ) : ContDiff ℝ (↑⊤) (floorChartAmplitude A η ρ)

theorem TrilinearHT.Auto.floorChartAmplitude_support_subset {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) {H : ℝ} (hH : 0 < H) (hA : ∀ (z : Fin d → ℝ), A.amplitude z ≠ 0 → ∀ (i : Fin d), |z i| ≤ H) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) : tsupport (floorChartAmplitude A η ρ) ⊆ Metric.closedBall 0 (H + ‖A.horizontal‖ + 1)

theorem TrilinearHT.Auto.floorChartAmplitude_compact {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) : HasCompactSupport (floorChartAmplitude A η ρ)

noncomputable def TrilinearHT.Auto.floorInterpolatedChart {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hηsm : ContDiff ℝ (↑⊤) η) (hρsm : ContDiff ℝ (↑⊤) ρ) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) : QuadraticChartData (d + 2)

Smooth chart realizing the floor-interpolated original atom in two extra dimensions.

Equations

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

theorem TrilinearHT.Auto.floorChartTailMatrix_phase (z w : Fin 2 → ℝ) : chartMatrixPhase floorChartTailMatrix z w = -z 1 * w 0

theorem TrilinearHT.Auto.floorInterpolatedChart_phased_summand {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hηsm : ContDiff ℝ (↑⊤) η) (hρsm : ContDiff ℝ (↑⊤) ρ) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) (v : ℝ) (n : Fin d → ℤ) (m k : ℤ) : ↑(Real.fourierChar (A.quadratic * v ^ 2 + A.linear * v)) * quadraticChartLatticeSummand (floorInterpolatedChart A η ρ hηsm hρsm hη hρ) v (Fin.append n ![m, k]) = η (v - ↑m) * ρ (floorChartAlpha A * v - ↑k) * (↑(Real.fourierChar (A.quadratic * ↑m ^ 2 + A.linear * ↑m)) * quadraticChartLatticeSummand A (↑m) n)

theorem TrilinearHT.Auto.floorInterpolatedChart_atom {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hηsm : ContDiff ℝ (↑⊤) η) (hρsm : ContDiff ℝ (↑⊤) ρ) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) (hpartition : ∀ (r : ℝ), ∑' (k : ℤ), ρ (r - ↑k) = 1) (v : ℝ) : quadraticChartAtom (floorInterpolatedChart A η ρ hηsm hρsm hη hρ) v = η (Int.fract v) * quadraticChartAtom A ↑⌊v⌋

theorem TrilinearHT.Auto.floorInterpolatedChart_bounded {d : ℕ} (A : QuadraticChartData d) (η ρ : ℝ → ℂ) (hηsm : ContDiff ℝ (↑⊤) η) (hρsm : ContDiff ℝ (↑⊤) ρ) (hη : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρ : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) (hpartition : ∀ (r : ℝ), ∑' (k : ℤ), ρ (r - ↑k) = 1) (hηbound : ∀ (x : ℝ), ‖η x‖ ≤ 1) (hA : ∀ (n : ℤ), ‖quadraticChartAtom A ↑n‖ ≤ 1) : IsBoundedQuadraticChart (floorInterpolatedChart A η ρ hηsm hρsm hη hρ)

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

theorem TrilinearHT.Auto.linear_derivative_norm_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : E →L[ℝ] ℝ) {T : ℝ} (hT : 1 ≤ T) (hL : ‖L‖ ≤ T) (z : E) (hz : ‖z‖ ≤ T) (m : ℕ) : ‖iteratedFDeriv ℝ m (⇑L) z‖ ≤ T ^ 2

theorem TrilinearHT.Auto.linear_product_derivative_bound {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L K : E →L[ℝ] ℝ) {T : ℝ} (hT : 1 ≤ T) (hL : ‖L‖ ≤ T) (hK : ‖K‖ ≤ T) (z : E) (hz : ‖z‖ ≤ T) (m : ℕ) : ‖iteratedFDeriv ℝ m (fun (y : E) => L y * K y) z‖ ≤ T ^ 4 * 2 ^ m

theorem TrilinearHT.Auto.quadratic_linear_phase_derivative_geometric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L K J : E →L[ℝ] ℝ) {T : ℝ} (hT : 1 ≤ T) (hL : ‖L‖ ≤ T) (hK : ‖K‖ ≤ T) (hJ : ‖J‖ ≤ T) (z : E) (hz : ‖z‖ ≤ T) (m i : ℕ) (hi : i ≤ m) : ‖iteratedFDeriv ℝ i (fun (y : E) => ↑(Real.fourierChar (L y * K y + J y))) z‖ ≤ (8 * Real.pi * T ^ 4 * (↑m + 1)) ^ i

theorem TrilinearHT.Auto.four_factor_derivative_geometric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g h k : E → ℂ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hh : ContDiff ℝ (↑⊤) h) (hk : ContDiff ℝ (↑⊤) k) (z : E) {m : ℕ} {R : ℝ} (hR : 0 ≤ R) (hfi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i f z‖ ≤ R ^ (i + 1)) (hgi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i g z‖ ≤ R ^ (i + 1)) (hhi : ∀ i ≤ m, ‖iteratedFDeriv ℝ i h z‖ ≤ R ^ (i + 1)) (hki : ∀ i ≤ m, ‖iteratedFDeriv ℝ i k z‖ ≤ R ^ (i + 1)) : ‖iteratedFDeriv ℝ m (fun (y : E) => f y * g y * h y * k y) z‖ ≤ R ^ 4 * (4 * R) ^ m

theorem TrilinearHT.Auto.four_factor_gevrey_budget {T : ℝ} (hT : 4 ≤ T) (a m : ℕ) (ha : 1 ≤ a) : (T ^ a * (↑m + 1) ^ a) ^ 4 * (4 * (T ^ a * (↑m + 1) ^ a)) ^ m ≤ T ^ (5 * a * (m + 1)) * (↑m + 1) ^ (5 * a * (m + 1))

noncomputable def TrilinearHT.Auto.floorChartShear {d : ℕ} (A : QuadraticChartData d) : (Fin (d + 2) → ℝ) →L[ℝ] Fin d → ℝ

Continuous linear shear removing the added translation coordinate from the chart coordinates.

Equations

• TrilinearHT.Auto.floorChartShear A = ContinuousLinearMap.pi fun (i : Fin d) => ContinuousLinearMap.proj (Fin.castAdd 2 i) - A.horizontal i • ContinuousLinearMap.proj (Fin.natAdd d 0)

theorem TrilinearHT.Auto.floorChartShear_norm_le {d : ℕ} (A : QuadraticChartData d) : ‖floorChartShear A‖ ≤ 1 + ‖A.horizontal‖

theorem TrilinearHT.Auto.chart_cutoff_linear_geometric {d D c₀ : ℕ} {H T : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hHT : H ≤ T) (L : (Fin D → ℝ) →L[ℝ] Fin d → ℝ) (hL : ‖L‖ ≤ T) (m i : ℕ) (hi : i ≤ m) (z : Fin D → ℝ) : ‖iteratedFDeriv ℝ i (A.amplitude ∘ ⇑L) z‖ ≤ (T ^ (2 * c₀ + 1) * (↑m + 1) ^ c₀) ^ (i + 1)

noncomputable def TrilinearHT.Auto.floorChartPhaseLinear {d : ℕ} (A : QuadraticChartData d) : (Fin (d + 2) → ℝ) →L[ℝ] ℝ

Continuous linear contribution to the floor-interpolation phase.

Equations

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

noncomputable def TrilinearHT.Auto.floorChartPhaseTail {d : ℕ} (A : QuadraticChartData d) : (Fin (d + 2) → ℝ) →L[ℝ] ℝ

Remaining linear phase carried by the added translation coordinate.

Equations

• TrilinearHT.Auto.floorChartPhaseTail A = -A.linear • ContinuousLinearMap.proj (Fin.natAdd d 0)

theorem TrilinearHT.Auto.floorChartPhase_eq {d : ℕ} (A : QuadraticChartData d) (z : Fin (d + 2) → ℝ) : z (Fin.natAdd d 0) * (floorChartPhaseLinear A) z + (floorChartPhaseTail A) z = (-z (Fin.natAdd d 0) * chartMatrixPhase A.matrix A.horizontal fun (i : Fin d) => z (Fin.castAdd 2 i)) + (A.quadratic + chartMatrixPhase A.matrix A.horizontal A.horizontal) * z (Fin.natAdd d 0) ^ 2 - A.linear * z (Fin.natAdd d 0)

theorem TrilinearHT.Auto.floorChartAmplitude_derivative_local {d c₀ K : ℕ} {H T : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hT : 32 ≤ T) (hHT : H ≤ T) (η ρ : ℝ → ℂ) (hη : ContDiff ℝ (↑⊤) η) (hρ : ContDiff ℝ (↑⊤) ρ) (hηd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i η x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) (hρd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i ρ x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) (hS : ‖floorChartShear A‖ ≤ T) (hL : ‖floorChartPhaseLinear A‖ ≤ T) (hJ : ‖floorChartPhaseTail A‖ ≤ T) (z : Fin (d + 2) → ℝ) (hz : ‖z‖ ≤ T) (m : ℕ) : ‖iteratedFDeriv ℝ m (floorChartAmplitude A η ρ) z‖ ≤ T ^ (5 * (2 * c₀ + K + 6) * (m + 1)) * (↑m + 1) ^ (5 * (2 * c₀ + K + 6) * (m + 1))

theorem TrilinearHT.Auto.floorChartAmplitude_derivative_bound {d c₀ K : ℕ} {H T : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hT : 32 ≤ T) (hHT : H ≤ T) (hsupp : H + ‖A.horizontal‖ + 1 ≤ T) (η ρ : ℝ → ℂ) (hη : ContDiff ℝ (↑⊤) η) (hρ : ContDiff ℝ (↑⊤) ρ) (hηs : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρs : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) (hηd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i η x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) (hρd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i ρ x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) (hS : ‖floorChartShear A‖ ≤ T) (hL : ‖floorChartPhaseLinear A‖ ≤ T) (hJ : ‖floorChartPhaseTail A‖ ≤ T) (m : ℕ) (word : Fin m → Fin (d + 2)) (z : Fin (d + 2) → ℝ) : ‖coordinateWordDerivative m (floorChartAmplitude A η ρ) word z‖ ≤ T ^ (5 * (2 * c₀ + K + 6) * (m + 1)) * (↑m + 1) ^ (5 * (2 * c₀ + K + 6) * (m + 1))

theorem TrilinearHT.Auto.chart_coordinate_projection_norm_le {D : ℕ} (i : Fin D) : ‖ContinuousLinearMap.proj i‖ ≤ 1

theorem TrilinearHT.Auto.floorChartPhaseLinear_norm_le {d : ℕ} (A : QuadraticChartData d) : ‖floorChartPhaseLinear A‖ ≤ ‖chartMatrixLeftLinear A.matrix A.horizontal‖ + |A.quadratic + chartMatrixPhase A.matrix A.horizontal A.horizontal|

theorem TrilinearHT.Auto.floorChartPhaseTail_norm_le {d : ℕ} (A : QuadraticChartData d) : ‖floorChartPhaseTail A‖ ≤ |A.linear|

theorem TrilinearHT.Auto.floor_chart_parameter_controls {d c₀ : ℕ} {H P : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hP : 0 ≤ P) (hPH : P ≤ H ^ d ^ 2) (hθ : ∀ (i : Fin d), |A.horizontal i| ≤ P) (hlam : |A.quadratic| ≤ 1) (hβ : |A.linear| ≤ 1) : 32 ≤ chartTranslationBase d H ^ 6 ∧ H ≤ chartTranslationBase d H ^ 6 ∧ H + ‖A.horizontal‖ + 1 ≤ chartTranslationBase d H ^ 6 ∧ ‖floorChartShear A‖ ≤ chartTranslationBase d H ^ 6 ∧ ‖floorChartPhaseLinear A‖ ≤ chartTranslationBase d H ^ 6 ∧ ‖floorChartPhaseTail A‖ ≤ chartTranslationBase d H ^ 6

theorem TrilinearHT.Auto.floorInterpolatedChart_complexity {d c₀ K : ℕ} {H P T : ℝ} {A : QuadraticChartData d} (hA : QuadraticChartComplexity c₀ H A) (hc : 1 ≤ c₀) (hP : 0 ≤ P) (hPH : P ≤ H ^ d ^ 2) (hθ : ∀ (i : Fin d), |A.horizontal i| ≤ P) (hlam : |A.quadratic| ≤ 1) (hβ : |A.linear| ≤ 1) (hBT : chartTranslationBase d H ^ 6 ≤ T) (η ρ : ℝ → ℂ) (hη : ContDiff ℝ (↑⊤) η) (hρ : ContDiff ℝ (↑⊤) ρ) (hηs : ∀ (x : ℝ), η x ≠ 0 → x ∈ Set.Ioo 0 1) (hρs : ∀ (x : ℝ), ρ x ≠ 0 → x ∈ Set.Ioo (-1) 1) (hηd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i η x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) (hρd : ∀ (i : ℕ) (x : ℝ), ‖iteratedDeriv i ρ x‖ ≤ T ^ (K * (i + 1)) * (↑i + 1) ^ (K * (i + 1))) : QuadraticChartComplexity (5 * (2 * c₀ + K + 6)) T (floorInterpolatedChart A η ρ hη hρ hηs hρs)

theorem TrilinearHT.Auto.complex_ofReal_iteratedDeriv_norm (f : ℝ → ℝ) (hf : ContDiff ℝ (↑⊤) f) (m : ℕ) (x : ℝ) : ‖iteratedDeriv m (fun (y : ℝ) => ↑(f y)) x‖ = |iteratedDeriv m f x|

theorem TrilinearHT.Auto.quadraticChart_uniform_floor_interpolation (c₀ : ℕ) (hc : 1 ≤ c₀) : ∃ (c₁ : ℕ) (B : ℝ), 1 ≤ c₁ ∧ 8 ≤ B ∧ ∀ (d : ℕ) (H ε : ℝ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ H A → (∃ (P : ℝ), 0 ≤ P ∧ P ≤ H ^ d ^ 2 ∧ ∀ (i : Fin d), |A.horizontal i| ≤ P) → |A.quadratic| ≤ 1 → |A.linear| ≤ 1 → (∀ (n : ℤ), ‖quadraticChartAtom A ↑n‖ ≤ 1) → 0 < ε → ε ≤ 1 / 2 → ∃ (η : ℝ → ℝ) (A' : QuadraticChartData (d + 2)), ContDiff ℝ (↑⊤) η ∧ (∀ (x : ℝ), η x ∈ Set.Icc 0 1) ∧ tsupport η ⊆ Set.Ioo 0 1 ∧ (∀ x ∈ Set.Icc ε (1 - ε), η x = 1) ∧ QuadraticChartComplexity c₁ (chartTranslationBudget H * (B / ε)) A' ∧ IsBoundedQuadraticChart A' ∧ ∀ (v : ℝ), quadraticChartAtom A' v = ↑(η (Int.fract v)) * quadraticChartAtom A ↑⌊v⌋

theorem TrilinearHT.Auto.monomial_uniform_natural_envelope (a : ℝ) (n : ℕ) : ∃ (D : ℕ), 1 ≤ D ∧ n ≤ D ∧ a ≤ ↑D ∧ ∀ (X : ℝ), 1 ≤ X → a * X ^ n ≤ ↑D * X ^ D

theorem TrilinearHT.Auto.uniform_floor_inverse_budget (C : ℕ) (hC : 1 ≤ C) (B : ℝ) (hB : 8 ≤ B) : ∃ (D : ℕ), 1 ≤ D ∧ ∀ (X : ℝ), 1 ≤ X → have H := Real.exp (↑C * X ^ C); have T := chartTranslationBudget H * (8 * B * H); T ≤ Real.exp (↑D * X ^ D) ∧ chartTranslationBudget T ≤ Real.exp (↑D * X ^ D) ∧ 2 * H ≤ Real.exp (↑D * X ^ D)

theorem TrilinearHT.Auto.quadraticChartAtom_measurable {d : ℕ} (A : QuadraticChartData d) : Measurable (quadraticChartAtom A)

noncomputable def TrilinearHT.Auto.inverseDecompositionBudget (C : ℕ) (t : ℝ) : ℝ

Quasipolynomial budget for the inverse-theorem atomic decomposition.

Equations

• TrilinearHT.Auto.inverseDecompositionBudget C t = 2 * (Real.exp 2 + Real.exp (↑C * (1 + Real.log (4 * t ^ 2)) ^ C))

theorem TrilinearHT.Auto.inverseDecompositionBudget_quasipolynomial {C : ℕ} (hC : 1 ≤ C) : QuasipolynomialBound (inverseDecompositionBudget C)

theorem TrilinearHT.Auto.inverseDecompositionBudget_at_reciprocal (C : ℕ) (τ : ℝ) : inverseDecompositionBudget C (1 / τ) = 2 * (Real.exp 2 + Real.exp (↑C * (1 + Real.log (1 / (τ / 2) ^ 2)) ^ C))

theorem TrilinearHT.Auto.quasipolynomialBound_of_le {f g : ℝ → ℝ} (hg : QuasipolynomialBound g) (hf0 : ∀ (t : ℝ), 2 ≤ t → 0 ≤ f t) (hfg : ∀ (t : ℝ), 2 ≤ t → f t ≤ g t) : QuasipolynomialBound f

theorem TrilinearHT.Auto.quasipolynomialBound_id : QuasipolynomialBound fun (t : ℝ) => t

theorem TrilinearHT.Auto.quasipolynomialBound_logarithmicSize : QuasipolynomialBound logarithmicSize

theorem TrilinearHT.Auto.quasipolynomialBound_natPow {f : ℝ → ℝ} (hf : QuasipolynomialBound f) (n : ℕ) : QuasipolynomialBound fun (t : ℝ) => f t ^ n

theorem TrilinearHT.Auto.quasipolynomialBound_logPower {f g : ℝ → ℝ} (hf : QuasipolynomialBound f) {C : ℝ} (hC : 1 ≤ C) (n : ℕ) (hg0 : ∀ (t : ℝ), 2 ≤ t → 0 ≤ g t) (hg : ∀ (t : ℝ), 2 ≤ t → g t ≤ C * logarithmicSize t ^ n) : QuasipolynomialBound fun (t : ℝ) => f t ^ g t

A power whose exponent is polynomial in logarithmic size preserves quasipolynomial growth.

noncomputable def TrilinearHT.Auto.shortReturnAlternatingBudget (t : ℝ) : ℝ

Budget for the alternating component in a short-return splitting.

Equations

• TrilinearHT.Auto.shortReturnAlternatingBudget t = 2 * TrilinearHT.Auto.logarithmicSize t ^ 2 * t

noncomputable def TrilinearHT.Auto.shortReturnRadiusBudget (t : ℝ) : ℝ

Radius budget for the short-return body.

Equations

• TrilinearHT.Auto.shortReturnRadiusBudget t = t + 100 * (t + TrilinearHT.Auto.shortReturnAlternatingBudget t + 1)

noncomputable def TrilinearHT.Auto.shortReturnGapBudget (t : ℝ) : ℝ

Gap between successive scales in the short-return construction.

Equations

• TrilinearHT.Auto.shortReturnGapBudget t = 16 * (100 * (TrilinearHT.Auto.logarithmicSize t + 1)) ^ (10 * (TrilinearHT.Auto.logarithmicSize t + 1))

noncomputable def TrilinearHT.Auto.shortReturnInitialScaleBudget (t : ℝ) : ℝ

Initial scale budget in the short-return construction.

Equations

• TrilinearHT.Auto.shortReturnInitialScaleBudget t = 100 + 100 * t * (TrilinearHT.Auto.logarithmicSize t + 4) * TrilinearHT.Auto.shortReturnRadiusBudget t

noncomputable def TrilinearHT.Auto.shortReturnScaleBudget (t : ℝ) : ℝ

Largest scale used by the short-return construction.

Equations

• TrilinearHT.Auto.shortReturnScaleBudget t = TrilinearHT.Auto.shortReturnInitialScaleBudget t * TrilinearHT.Auto.shortReturnGapBudget t ^ (TrilinearHT.Auto.logarithmicSize t + 1)

noncomputable def TrilinearHT.Auto.shortReturnRowBudget (t : ℝ) : ℝ

Row budget determined by the short-return scale.

Equations

• TrilinearHT.Auto.shortReturnRowBudget t = 2 + TrilinearHT.Auto.shortReturnScaleBudget t

noncomputable def TrilinearHT.Auto.shortReturnProjectionBudget (t : ℝ) : ℝ

Budget for the projections used in short-return splitting.

Equations

• TrilinearHT.Auto.shortReturnProjectionBudget t = (2 * TrilinearHT.Auto.shortReturnRowBudget t) ^ (8 * (TrilinearHT.Auto.logarithmicSize t + 1) ^ 4)

noncomputable def TrilinearHT.Auto.shortReturnGramBudget (t : ℝ) : ℝ

Gram-matrix budget for the short-return rows.

Equations

• TrilinearHT.Auto.shortReturnGramBudget t = 2 + TrilinearHT.Auto.logarithmicSize t * TrilinearHT.Auto.shortReturnRowBudget t ^ 2

noncomputable def TrilinearHT.Auto.shortReturnSlowBudget (t : ℝ) : ℝ

Budget for the slowly varying component of a short return.

Equations

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

noncomputable def TrilinearHT.Auto.shortReturnTimeInverseBudget (t : ℝ) : ℝ

Inverse time-scale budget for the short-return phase estimates.

Equations

• TrilinearHT.Auto.shortReturnTimeInverseBudget t = (1 + 4 * TrilinearHT.Auto.shortReturnScaleBudget t) ^ TrilinearHT.Auto.logarithmicSize t * TrilinearHT.Auto.shortReturnScaleBudget t

noncomputable def TrilinearHT.Auto.shortReturnQuadraticBudget (t : ℝ) : ℝ

Budget for the quadratic phase remaining after short-return splitting.

Equations

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

noncomputable def TrilinearHT.Auto.shortReturnSplittingBudget (t : ℝ) : ℝ

Combined projection, slow-component and quadratic budgets for short-return splitting.

Equations

• TrilinearHT.Auto.shortReturnSplittingBudget t = 2 + TrilinearHT.Auto.shortReturnProjectionBudget t + TrilinearHT.Auto.shortReturnSlowBudget t + TrilinearHT.Auto.shortReturnQuadraticBudget t

theorem TrilinearHT.Auto.shortReturnAlternatingBudget_quasipolynomial : QuasipolynomialBound shortReturnAlternatingBudget

theorem TrilinearHT.Auto.shortReturnRadiusBudget_quasipolynomial : QuasipolynomialBound shortReturnRadiusBudget

theorem TrilinearHT.Auto.shortReturnGapBudget_quasipolynomial : QuasipolynomialBound shortReturnGapBudget

theorem TrilinearHT.Auto.shortReturnScaleBudget_quasipolynomial : QuasipolynomialBound shortReturnScaleBudget

theorem TrilinearHT.Auto.shortReturnRowBudget_quasipolynomial : QuasipolynomialBound shortReturnRowBudget

theorem TrilinearHT.Auto.logarithmicSize_add_one_pow_four {t : ℝ} (ht : 2 ≤ t) : (logarithmicSize t + 1) ^ 4 ≤ 16 * logarithmicSize t ^ 4

theorem TrilinearHT.Auto.shortReturnProjectionBudget_quasipolynomial : QuasipolynomialBound shortReturnProjectionBudget

theorem TrilinearHT.Auto.shortReturnGramBudget_quasipolynomial : QuasipolynomialBound shortReturnGramBudget

theorem TrilinearHT.Auto.shortReturnSlowBudget_quasipolynomial : QuasipolynomialBound shortReturnSlowBudget

theorem TrilinearHT.Auto.shortReturnTimeInverseBudget_quasipolynomial : QuasipolynomialBound shortReturnTimeInverseBudget

theorem TrilinearHT.Auto.shortReturnQuadraticBudget_quasipolynomial : QuasipolynomialBound shortReturnQuadraticBudget

theorem TrilinearHT.Auto.quasipolynomialBound_nonneg {f : ℝ → ℝ} (hf : QuasipolynomialBound f) {t : ℝ} (ht : 2 ≤ t) : 0 ≤ f t

theorem TrilinearHT.Auto.continuous_inverse_sample_witness : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (δ : ℝ), 0 < δ → δ < 1 / 2 → ∀ (g : ℝ → ℂ), Measurable g → (∀ (x : ℝ), ‖g x‖ ≤ 1) → (∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Icc 0 1) → δ ≤ gowersNorm AddCircle.haarAddCircle 3 (AddCircle.liftIoc 16 (-8) g) → ∃ (L : ℕ) (d : ℕ) (A : QuadraticChartData d), 0 < L ∧ QuadraticChartComplexity c₀ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C)) A ∧ IsBoundedQuadraticChart A ∧ (Real.exp (↑C * (1 + Real.log (1 / δ)) ^ C))⁻¹ ≤ ‖∑ k ∈ Finset.range L, (∫ (x : ℝ) in ↑k / ↑L..(↑k + 1) / ↑L, g x) * (starRingEnd ℂ) (quadraticChartAtom A ↑k)‖

Blueprint lem:inverse, lines 1191–1195: after choosing a sufficiently fine cyclic discretization, a globally bounded quadratic chart correlates with the original input's cell integrals, with a uniform quasipolynomial budget.

theorem TrilinearHT.Auto.continuous_inverse_affine_coordinates : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (δ : ℝ), 0 < δ → δ < 1 / 2 → ∀ (g : ℝ → ℂ), Measurable g → (∀ (x : ℝ), ‖g x‖ ≤ 1) → (∀ (x : ℝ), g x ≠ 0 → x ∈ Set.Icc 0 1) → δ ≤ gowersNorm AddCircle.haarAddCircle 3 (AddCircle.liftIoc 16 (-8) g) → ∀ (s t : ℝ), s ≠ 0 → ∃ (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))⁻¹ ≤ ‖∫ (x : ℝ) in 0..1, g x * (starRingEnd ℂ) (quadraticChartAtom A (s * x + t))‖

theorem TrilinearHT.Auto.continuous_inverse : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (a b : ℝ), a < b → ∀ (δ : ℝ), 0 < δ → δ < 1 / 2 → ∀ (f : ℝ → ℂ), Measurable f → (∀ x ∈ Set.Ico a b, ‖f x‖ ≤ 1) → δ ≤ intervalGowersNorm a b 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))⁻¹ ≤ (b - a)⁻¹ * ‖∫ (x : ℝ) in a..b, f x * (starRingEnd ℂ) (quadraticChartAtom A x)‖

Blueprint lem:inverse, continuous inverse statement on every nondegenerate interval, with uniform Gevrey order and quasipolynomial complexity/correlation.

theorem TrilinearHT.Auto.continuous_decomposition_interval : ∃ (c₀ : ℕ) (C : ℕ), 1 ≤ c₀ ∧ 1 ≤ C ∧ ∀ (left right : ℝ), left < right → ∀ (τ : ℝ), 0 < τ → τ < 1 / 2 → ∀ (f : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))), (∀ᵐ (x : ℝ) ∂intervalProbabilityMeasure left right, ‖↑↑f x‖ ≤ 1) → ∃ (ι : Type) (s : Finset ι) (c : ι → ℂ) (a : ι → ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))) (u : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))) (v : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))), (∀ i ∈ s, ∃ (d : ℕ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ (Real.exp 2 + Real.exp (↑C * (1 + Real.log (1 / (τ / 2) ^ 2)) ^ C)) A ∧ IsBoundedQuadraticChart A ∧ ↑↑(a i) =ᵐ[intervalProbabilityMeasure left right] quadraticChartAtom A) ∧ ∑ i ∈ s, ‖c i‖ ≤ 2 * (Real.exp 2 + Real.exp (↑C * (1 + Real.log (1 / (τ / 2) ^ 2)) ^ C)) ∧ (intervalL2GowersSeminorm left right) u ≤ τ ∧ probabilityL2L1Norm (intervalProbabilityMeasure left right) v ≤ τ ∧ f = ∑ i ∈ s, c i • a i + u + v

Blueprint lem:inverse: the finite decomposition on every nondegenerate interval with probability normalization and uniform explicit quantitative bounds.

theorem TrilinearHT.Auto.continuous_decomposition : ∃ (c₀ : ℕ) (D : ℝ → ℝ), 1 ≤ c₀ ∧ QuasipolynomialBound D ∧ ∀ (left right : ℝ), left < right → ∀ (τ : ℝ), 0 < τ → τ < 1 / 2 → ∀ (f : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))), (∀ᵐ (x : ℝ) ∂intervalProbabilityMeasure left right, ‖↑↑f x‖ ≤ 1) → ∃ (ι : Type) (s : Finset ι) (c : ι → ℂ) (a : ι → ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))) (u : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))) (v : ↥(MeasureTheory.Lp ℂ 2 (intervalProbabilityMeasure left right))), (∀ i ∈ s, ∃ (d : ℕ) (A : QuadraticChartData d), QuadraticChartComplexity c₀ (D (1 / τ)) A ∧ IsBoundedQuadraticChart A ∧ ↑↑(a i) =ᵐ[intervalProbabilityMeasure left right] quadraticChartAtom A) ∧ ∑ i ∈ s, ‖c i‖ ≤ D (1 / τ) ∧ (intervalL2GowersSeminorm left right) u ≤ τ ∧ probabilityL2L1Norm (intervalProbabilityMeasure left right) v ≤ τ ∧ f = ∑ i ∈ s, c i • a i + u + v

Blueprint lem:inverse, decomposition assertion: every unit-bounded L2 input on a nondegenerate interval is a finite sum of bounded quadratic chart atoms, a U3 error and an L1 error. One quasipolynomial budget controls both chart complexity and the sum of coefficient magnitudes, uniformly in the interval.