Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Additivity.AnalyticInequalities

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

AdditivityAnalyticInequalities

Finite-measure Cauchy inequalities for the additivity-cross term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.additivitySumHalfEnergyDensityOnFamilyOnCube_integrableOn {d : ℕ} [NeZero d] (a : Ch02.TriadicCoeffFamily d) (Q : TriadicCube d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) : MeasureTheory.IntegrableOn (additivitySumHalfEnergyDensityOnFamilyOnCube a Q R p q) (cubeSet R) MeasureTheory.volume

The local sum half-energy density is locally integrable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.memLp_sqrt_two_of_integrable_of_ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf_int : MeasureTheory.Integrable f μ) (hf_nonneg : 0 ≤ᵐ[μ] f) : MeasureTheory.MemLp (fun (x : α) => √(f x)) 2 μ

An integrable nonnegative scalar density has a square root in normalized L².

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_sqrt_mul_sqrt_le_sqrt_integral_mul_sqrt_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A B : α → ℝ} (hA_int : MeasureTheory.Integrable A μ) (hB_int : MeasureTheory.Integrable B μ) (hA_nonneg : 0 ≤ᵐ[μ] A) (hB_nonneg : 0 ≤ᵐ[μ] B) : ∫ (x : α), √(A x) * √(B x) ∂μ ≤ √(∫ (x : α), A x ∂μ) * √(∫ (x : α), B x ∂μ)

Cauchy-Schwarz for square roots of nonnegative integrable scalar observables, in the form used by the stochastic additivity term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrable_sqrt_mul_sqrt_of_integrable_of_ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {A B : α → ℝ} (hA_int : MeasureTheory.Integrable A μ) (hB_int : MeasureTheory.Integrable B μ) (hA_nonneg : 0 ≤ᵐ[μ] A) (hB_nonneg : 0 ≤ᵐ[μ] B) : MeasureTheory.Integrable (fun (x : α) => √(A x) * √(B x)) μ

Integrability companion to the square-root Cauchy estimate.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrable_mul_of_integrable_sq_of_ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {X Y : α → ℝ} (hX_sq : MeasureTheory.Integrable (fun (x : α) => X x ^ 2) μ) (hY_sq : MeasureTheory.Integrable (fun (x : α) => Y x ^ 2) μ) (hX_nonneg : 0 ≤ᵐ[μ] X) (hY_nonneg : 0 ≤ᵐ[μ] Y) : MeasureTheory.Integrable (fun (x : α) => X x * Y x) μ

Integrability of a nonnegative product from square integrability of both factors.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_mul_le_sqrt_integral_sq_mul_sqrt_integral_sq_of_ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {X Y : α → ℝ} (hX_sq : MeasureTheory.Integrable (fun (x : α) => X x ^ 2) μ) (hY_sq : MeasureTheory.Integrable (fun (x : α) => Y x ^ 2) μ) (hX_nonneg : 0 ≤ᵐ[μ] X) (hY_nonneg : 0 ≤ᵐ[μ] Y) : ∫ (x : α), X x * Y x ∂μ ≤ √(∫ (x : α), X x ^ 2 ∂μ) * √(∫ (x : α), Y x ^ 2 ∂μ)

Cauchy-Schwarz in the form needed for the manuscript product of the two scaled weak norms.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.abs_cubeAverage_le_sqrt_cubeAverage_mul_sqrt_cubeAverage_of_ae_abs_le_sqrt_mul_sqrt {d : ℕ} (Q : TriadicCube d) {F A B : Vec d → ℝ} (hF_int : MeasureTheory.Integrable F (normalizedCubeMeasure Q)) (hA_nonneg : 0 ≤ᵐ[normalizedCubeMeasure Q] A) (hB_nonneg : 0 ≤ᵐ[normalizedCubeMeasure Q] B) (hSqrtA_mem : MeasureTheory.MemLp (fun (x : Vec d) => √(A x)) 2 (normalizedCubeMeasure Q)) (hSqrtB_mem : MeasureTheory.MemLp (fun (x : Vec d) => √(B x)) 2 (normalizedCubeMeasure Q)) (hPoint : ∀ᵐ (x : Vec d) ∂normalizedCubeMeasure Q, |F x| ≤ √(A x) * √(B x)) : |cubeAverage Q F| ≤ √(cubeAverage Q A) * √(cubeAverage Q B)

If |F| ≤ sqrt A sqrt B a.e. on a normalized cube, then the cube average of F is bounded by the square roots of the cube averages of A and B.