Coarse-graining support: Support.Sobolev.FiniteLpCoordinate

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

Finite-p coordinate bounds for direct Euclidean fields

These inequalities compare the project-vector coordinate functions with the Euclidean Hilbert realization HilbertVec.ofVec, while leaving the project's ambient product norm unchanged.

theorem HCPolySupport.ennreal_sum_rpow_le_rpow_sum {ι : Type u_1} [Fintype ι] (a : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) : ∑ i : ι, a i ^ p ≤ (∑ i : ι, a i) ^ p

For a finite family of extended nonnegative reals and an exponent at least one, the sum of the powers is bounded by the power of the sum.

theorem HCPolySupport.ennreal_rpow_sum_le_card_rpow_mul_sum_rpow {ι : Type u_1} [Fintype ι] (a : ι → ENNReal) {p : ℝ} (hp : 1 ≤ p) : (∑ i : ι, a i) ^ p ≤ ↑(Fintype.card ι) ^ (p - 1) * ∑ i : ι, a i ^ p

For a finite family of extended nonnegative reals and an exponent at least one, the power of the sum is bounded by the cardinality Hölder factor times the sum of the powers.

theorem HCPolySupport.finiteLpExponent_sum_rpow_le_rpow_sum {ι : Type u_1} [Fintype ι] (a : ι → ENNReal) (p : FiniteLpExponent) : ∑ i : ι, a i ^ p.exponent.toReal ≤ (∑ i : ι, a i) ^ p.exponent.toReal

The lower finite-dimensional power-sum comparison at a campaign finite L^p exponent.

theorem HCPolySupport.finiteLpExponent_rpow_sum_le_card_rpow_mul_sum_rpow {ι : Type u_1} [Fintype ι] (a : ι → ENNReal) (p : FiniteLpExponent) : (∑ i : ι, a i) ^ p.exponent.toReal ≤ ↑(Fintype.card ι) ^ (p.exponent.toReal - 1) * ∑ i : ι, a i ^ p.exponent.toReal

The upper finite-dimensional power-sum comparison at a campaign finite L^p exponent, valid also when one of the summands is infinite.

theorem HCPolySupport.abs_coordinate_le_euclideanNorm {d : ℕ} (v : Vec d) (i : Fin d) : |v i| ≤ euclideanNorm v

A coordinate of a project vector is bounded by its explicit Euclidean magnitude.

theorem HCPolySupport.coordinate_eLpNorm_le_euclidean {α : Type u_1} [MeasurableSpace α] {d : ℕ} (μ : MeasureTheory.Measure α) (p : FiniteLpExponent) (F : α → Vec d) (i : Fin d) : MeasureTheory.eLpNorm (fun (x : α) => F x i) p.exponent μ ≤ MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p.exponent μ

The extended L^p norm of a scalar coordinate is bounded by that of the direct Euclidean Hilbert realization, without a measurability premise.

theorem HCPolySupport.sum_coordinate_eLpNorm_rpow_le_dimension_mul {α : Type u_1} [MeasurableSpace α] {d : ℕ} (μ : MeasureTheory.Measure α) (p : FiniteLpExponent) (F : α → Vec d) : ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : α) => F x i) p.exponent μ ^ p.exponent.toReal ≤ ↑d * MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p.exponent μ ^ p.exponent.toReal

The finite sum of coordinate p-powers is bounded by d times the direct Euclidean vector p-power.

theorem HCPolySupport.euclidean_eLpNorm_le_dimension_mul_sum_coordinates {α : Type u_1} [MeasurableSpace α] {d : ℕ} (μ : MeasureTheory.Measure α) (p : FiniteLpExponent) (F : α → Vec d) (hcoord : ∀ (i : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : α) => F x i) μ) : MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p.exponent μ ≤ ‖↑d‖ₑ * ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : α) => F x i) p.exponent μ

A direct Euclidean vector L^p norm is bounded by a dimension factor times the finite sum of coordinate L^p norms.

theorem HCPolySupport.euclidean_eLpNorm_rpow_le_dimension_sum_rpow {α : Type u_1} [MeasurableSpace α] {d : ℕ} (μ : MeasureTheory.Measure α) (p : FiniteLpExponent) (F : α → Vec d) (hcoord : ∀ (i : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : α) => F x i) μ) : MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p.exponent μ ^ p.exponent.toReal ≤ (‖↑d‖ₑ * ∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : α) => F x i) p.exponent μ) ^ p.exponent.toReal

Raising the coordinate-sum upper bound to the finite p power.

theorem HCPolySupport.euclidean_eLpNorm_rpow_le_dimension_rpow_mul_sum_rpow {α : Type u_1} [MeasurableSpace α] {d : ℕ} (μ : MeasureTheory.Measure α) (p : FiniteLpExponent) (F : α → Vec d) (hcoord : ∀ (i : Fin d), MeasureTheory.AEStronglyMeasurable (fun (x : α) => F x i) μ) : MeasureTheory.eLpNorm (fun (x : α) => HilbertVec.ofVec (F x)) p.exponent μ ^ p.exponent.toReal ≤ ‖↑d‖ₑ ^ p.exponent.toReal * (∑ i : Fin d, MeasureTheory.eLpNorm (fun (x : α) => F x i) p.exponent μ) ^ p.exponent.toReal

Expanded finite-p form of the coordinate-sum upper bound.