Iterates L2Finite Triangle

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.IteratesL2FiniteTriangle.quadratic_cross_bound {A B R : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hp : ∀ (t : ℝ), 0 ≤ t ^ 2 * A - 2 * t * R + B) : R ≤ √A * √B

theorem AVenhance.Infra.Section4.iterate_vector_integral_L2_add {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → Homogenization.Vec 2} (hf : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecNormSq (f x)) μ) (hg : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecNormSq (g x)) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => Homogenization.vecDot (f x) (g x)) μ) : √(∫ (x : α), Homogenization.vecNormSq (f x + g x) ∂μ) ≤ √(∫ (x : α), Homogenization.vecNormSq (f x) ∂μ) + √(∫ (x : α), Homogenization.vecNormSq (g x) ∂μ)

The integral L2 triangle inequality for the actual Vec 2 carrier.

theorem AVenhance.Infra.Section4.iterate_vector_integral_L2_sum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} {S : Set α} (s : Finset ι) (f : ι → α → Homogenization.Vec 2) (hf : ∀ i ∈ s, ContinuousOn (f i) S) (hI : ∀ (q : α → ℝ), ContinuousOn q S → MeasureTheory.Integrable q μ) : √(∫ (x : α), Homogenization.vecNormSq (∑ i ∈ s, f i x) ∂μ) ≤ ∑ i ∈ s, √(∫ (x : α), Homogenization.vecNormSq (f i x) ∂μ)

Finite sums on a compact integration domain obey the L2 triangle inequality. The integrability supplier is used on continuous scalar polynomials only.

theorem AVenhance.Infra.Section4.iterate_scalar_integral_L2_sum {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [TopologicalSpace α] {μ : MeasureTheory.Measure α} {S : Set α} (s : Finset ι) (f : ι → α → ℝ) (hf : ∀ i ∈ s, ContinuousOn (f i) S) (hI : ∀ (q : α → ℝ), ContinuousOn q S → MeasureTheory.Integrable q μ) : √(∫ (x : α), (∑ i ∈ s, f i x) ^ 2 ∂μ) ≤ ∑ i ∈ s, √(∫ (x : α), f i x ^ 2 ∂μ)

Scalar finite-sum triangle inequality, without a dimension loss.