This file was automatically generated by Codex.

Hilbert-space atomic decomposition

General normalized convex separation and dual seminorm bounds for the atomic decomposition in lem:inverse, blueprint lines 1218-1239. All statements use Mathlib and definitions in this module.

theorem TrilinearHT.Auto.hilbert_separate_convex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {S : Set E} (hS : Convex ℝ S) (hzero : 0 ∈ S) {f : E} (hf : f ∉ closure S) : ∃ (h : E), 1 < (inner ℂ h f).re ∧ ∀ z ∈ S, (inner ℂ h z).re ≤ 1

theorem TrilinearHT.Auto.complex_norm_le_of_phase_re_le {w : ℂ} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (c : ℂ), ‖c‖ ≤ 1 → (c * w).re ≤ C) : ‖w‖ ≤ C

theorem TrilinearHT.Auto.inner_norm_le_of_balanced_re_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {S : Set E} (hS : Balanced ℂ S) {h z : E} (hz : z ∈ S) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ x ∈ S, (inner ℂ h x).re ≤ C) : ‖inner ℂ h z‖ ≤ C

theorem TrilinearHT.Auto.seminorm_bound_of_closedBall {E : Type u_1} [AddCommGroup E] [Module ℂ E] (p q : Seminorm ℂ E) {σ : ℝ} (hσ : 0 < σ) (hbound : ∀ (x : E), p x ≤ σ → q x ≤ 1) (x : E) : σ * q x ≤ p x

noncomputable def TrilinearHT.Auto.complexAtomicHull {E : Type u_1} [AddCommGroup E] [Module ℂ E] [Module ℝ E] (M : ℝ) (A : Set E) : Set E

Real convex hull of zero and complex multiples of atoms with coefficient norm at most M.

Equations

• TrilinearHT.Auto.complexAtomicHull M A = (convexHull ℝ) ({0} ∪ {z : E | ∃ a ∈ A, ∃ (c : ℂ), ‖c‖ ≤ M ∧ z = c • a})

theorem TrilinearHT.Auto.complexAtomicHull_zero {E : Type u_1} [AddCommGroup E] [Module ℂ E] [Module ℝ E] (M : ℝ) (A : Set E) : 0 ∈ complexAtomicHull M A

theorem TrilinearHT.Auto.complexAtomicHull_single {E : Type u_1} [AddCommGroup E] [Module ℂ E] [Module ℝ E] {M : ℝ} {A : Set E} {a : E} (ha : a ∈ A) {c : ℂ} (hc : ‖c‖ ≤ M) : c • a ∈ complexAtomicHull M A

noncomputable def TrilinearHT.Auto.atomicSeminormSum {E : Type u_1} [AddCommGroup E] [Module ℂ E] [Module ℝ E] (M σ : ℝ) (A : Set E) (p q : Seminorm ℂ E) : Set E

Atomic convex hull enlarged by closed balls of the two seminorms.

Equations

• TrilinearHT.Auto.atomicSeminormSum M σ A p q = TrilinearHT.Auto.complexAtomicHull M A + p.closedBall 0 σ + q.closedBall 0 σ

theorem TrilinearHT.Auto.atomicSeminormSum_convex {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M σ : ℝ) (A : Set E) (p q : Seminorm ℂ E) : Convex ℝ (atomicSeminormSum M σ A p q)

theorem TrilinearHT.Auto.atomicSeminormSum_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : ℝ) {σ : ℝ} (hσ : 0 ≤ σ) (A : Set E) (p q : Seminorm ℂ E) : 0 ∈ atomicSeminormSum M σ A p q

theorem TrilinearHT.Auto.inner_seminorm_ball_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : Seminorm ℂ E) {σ : ℝ} (hσ : 0 < σ) (h : E) (hb : ∀ z ∈ p.closedBall 0 σ, (inner ℂ h z).re ≤ 1) (x : E) : σ * ‖inner ℂ h x‖ ≤ p x

theorem TrilinearHT.Auto.atomicSeminormSum_separation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {M σ : ℝ} (hM : 0 ≤ M) (hσ : 0 < σ) (A : Set E) (p q : Seminorm ℂ E) {f : E} (hf : f ∉ closure (atomicSeminormSum M σ A p q)) : ∃ (h : E), 1 < (inner ℂ h f).re ∧ (∀ (x : E), σ * ‖inner ℂ h x‖ ≤ p x) ∧ (∀ (x : E), σ * ‖inner ℂ h x‖ ≤ q x) ∧ ∀ a ∈ A, M * ‖inner ℂ h a‖ ≤ 1

noncomputable def TrilinearHT.Auto.probabilityL2L1Norm {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : ℝ

Integral of the norm of an L² representative, used for the L¹ control seminorm.

Equations

• TrilinearHT.Auto.probabilityL2L1Norm μ f = ∫ (x : X), ‖↑↑f x‖ ∂μ

theorem TrilinearHT.Auto.probabilityL2L1Norm_eq {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : probabilityL2L1Norm μ f = ∫ (x : X), ‖↑↑f x‖ ∂μ

theorem TrilinearHT.Auto.probabilityL2L1Norm_add {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (f g : ↥(MeasureTheory.Lp ℂ 2 μ)) : probabilityL2L1Norm μ (f + g) ≤ probabilityL2L1Norm μ f + probabilityL2L1Norm μ g

theorem TrilinearHT.Auto.probabilityL2L1Norm_smul {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : probabilityL2L1Norm μ (c • f) = ‖c‖ * probabilityL2L1Norm μ f

noncomputable def TrilinearHT.Auto.probabilityL2L1Seminorm {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 μ)

Seminorm on L² induced by the integral of the pointwise norm.

Equations

• TrilinearHT.Auto.probabilityL2L1Seminorm μ = Seminorm.of (TrilinearHT.Auto.probabilityL2L1Norm μ) ⋯ ⋯

theorem TrilinearHT.Auto.probabilityL2L1_dual_ae_bound {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (h : ↥(MeasureTheory.Lp ℂ 2 μ)) {σ : ℝ} (hσ : 0 < σ) (hb : ∀ (u : ↥(MeasureTheory.Lp ℂ 2 μ)), σ * ‖inner ℂ h u‖ ≤ probabilityL2L1Norm μ u) : ∀ᵐ (x : X) ∂μ, ‖↑↑h x‖ ≤ σ⁻¹

theorem TrilinearHT.Auto.probabilityL2_atomic_separation {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {M σ : ℝ} (hM : 0 ≤ M) (hσ : 0 < σ) (A : Set ↥(MeasureTheory.Lp ℂ 2 μ)) (p : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 μ)) {f : ↥(MeasureTheory.Lp ℂ 2 μ)} (hf : f ∉ closure (atomicSeminormSum M σ A p (probabilityL2L1Seminorm μ))) : ∃ (h : ↥(MeasureTheory.Lp ℂ 2 μ)), 1 < (inner ℂ h f).re ∧ (∀ᵐ (x : X) ∂μ, ‖↑↑h x‖ ≤ σ⁻¹) ∧ (∀ (x : ↥(MeasureTheory.Lp ℂ 2 μ)), σ * ‖inner ℂ h x‖ ≤ p x) ∧ ∀ a ∈ A, M * ‖inner ℂ h a‖ ≤ 1

lem:inverse, lines 1225-1237: separation outside the closure of an atomic sum and two seminorm balls gives a normalized L2 separator, an essential supremum bound, the uniformity dual bound, and the atom pairing bound.

theorem TrilinearHT.Auto.probabilityL2_atomic_closure {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {M σ κ : ℝ} (hM : 0 ≤ M) (hσ : 0 < σ) (hcost : σ < M * κ) (A : Set ↥(MeasureTheory.Lp ℂ 2 μ)) (p : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 μ)) (hinverse : ∀ (g : ↥(MeasureTheory.Lp ℂ 2 μ)), (∀ᵐ (x : X) ∂μ, ‖↑↑g x‖ ≤ 1) → σ ^ 2 ≤ p g → ∃ a ∈ A, κ ≤ ‖inner ℂ g a‖) {f : ↥(MeasureTheory.Lp ℂ 2 μ)} (hf : ‖f‖ ≤ 1) : f ∈ closure (atomicSeminormSum M σ A p (probabilityL2L1Seminorm μ))

theorem TrilinearHT.Auto.probabilityL2L1Norm_le_norm {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : probabilityL2L1Norm μ f ≤ ‖f‖

theorem TrilinearHT.Auto.complexAtomicHull_finite {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {M : ℝ} (hM : 0 ≤ M) {A : Set E} (hA : A.Nonempty) {x : E} (hx : x ∈ complexAtomicHull M A) : ∃ (ι : Type) (s : Finset ι) (c : ι → ℂ) (a : ι → E), (∀ i ∈ s, a i ∈ A) ∧ ∑ i ∈ s, ‖c i‖ ≤ M ∧ ∑ i ∈ s, c i • a i = x

theorem TrilinearHT.Auto.probabilityL2_atomic_decomposition {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure μ] {M σ κ ε : ℝ} (hM : 0 ≤ M) (hσ : 0 < σ) (hε : 0 < ε) (hcost : σ < M * κ) (A : Set ↥(MeasureTheory.Lp ℂ 2 μ)) (hA : A.Nonempty) (p : Seminorm ℂ ↥(MeasureTheory.Lp ℂ 2 μ)) (hinverse : ∀ (g : ↥(MeasureTheory.Lp ℂ 2 μ)), (∀ᵐ (x : X) ∂μ, ‖↑↑g x‖ ≤ 1) → σ ^ 2 ≤ p g → ∃ a ∈ A, κ ≤ ‖inner ℂ g a‖) {f : ↥(MeasureTheory.Lp ℂ 2 μ)} (hf : ‖f‖ ≤ 1) : ∃ (ι : Type) (s : Finset ι) (c : ι → ℂ) (a : ι → ↥(MeasureTheory.Lp ℂ 2 μ)) (u : ↥(MeasureTheory.Lp ℂ 2 μ)) (v : ↥(MeasureTheory.Lp ℂ 2 μ)), (∀ i ∈ s, a i ∈ A) ∧ ∑ i ∈ s, ‖c i‖ ≤ M ∧ p u ≤ σ ∧ probabilityL2L1Norm μ v ≤ σ + ε ∧ f = ∑ i ∈ s, c i • a i + u + v