Coarse-graining support: Support.Sobolev.Fractional.EuclideanGagliardoCoordinateBridgeP

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

Finite-p Euclidean-to-coordinate Gagliardo bridge

This module separates the two elementary changes which occur in the finite exponent comparison: first replace the Euclidean distance in the vector kernel by the project's ambient distance, and then compare that Hilbert-vector kernel with its scalar coordinates. Every displayed constant is independent of the fractional order s ∈ (0,1).

noncomputable def HCPolySupport.cubeAmbientHilbertWspKernel {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : Vec d × Vec d → HilbertVec d

The intermediate ambient-distance, Euclidean-vector kernel. Its scalar coordinates are exactly the scalar Gagliardo kernels of the coordinates of F; only its distance differs from cubeEuclideanWspKernel.

Equations

• HCPolySupport.cubeAmbientHilbertWspKernel s p F z = dist z.1 z.2 ^ (-(↑s + ↑d / p.exponent.toReal)) • HCPolySupport.HilbertVec.ofVec (F z.1 - F z.2)

@[simp]

theorem HCPolySupport.cubeAmbientHilbertWspKernel_apply {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : cubeAmbientHilbertWspKernel s p F z = dist z.1 z.2 ^ (-(↑s + ↑d / p.exponent.toReal)) • HilbertVec.ofVec (F z.1 - F z.2)

noncomputable def HCPolySupport.cubeAmbientHilbertWspESeminorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : ENNReal

The finite-p seminorm of the intermediate ambient-distance vector kernel.

Equations

• HCPolySupport.cubeAmbientHilbertWspESeminorm Q s p F = MeasureTheory.eLpNorm (HCPolySupport.cubeAmbientHilbertWspKernel s p F) p.exponent (HCPolySupport.Gagliardo.gagliardoCubeMeasure Q)

theorem HCPolySupport.cubeAmbientHilbertWspESeminorm_eq_lintegral {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeAmbientHilbertWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeAmbientHilbertWspESeminorm Q s p F = (∫⁻ (z : Vec d × Vec d), ‖cubeAmbientHilbertWspKernel s p F z‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q) ^ (1 / p.exponent.toReal)

theorem HCPolySupport.cubeAmbientHilbertWspKernel_coordinate {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) (i : Fin d) : (cubeAmbientHilbertWspKernel s p F z).ofLp i = Gagliardo.gagliardoKernel (↑s) p.exponent (fun (x : Vec d) => F x i) z

The scalar coordinates of the intermediate vector kernel are precisely the scalar ambient-distance Gagliardo kernels.

theorem HCPolySupport.cubeEuclideanLp_coordinate_memLp {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => F.toField x i) p.exponent (normalizedCubeMeasure Q)

A direct Euclidean L^p field has scalar coordinate L^p fields on the same cube.

theorem HCPolySupport.cubeAmbientHilbertWspKernel_enorm_rpow {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : ‖cubeAmbientHilbertWspKernel s p F z‖ₑ ^ p.exponent.toReal = ENNReal.ofReal (dist z.1 z.2 ^ (-(↑s * p.exponent.toReal + ↑d))) * ENNReal.ofReal (euclideanNorm (F z.1 - F z.2) ^ p.exponent.toReal)

Exact powered-kernel identity for the intermediate ambient-distance Hilbert-vector kernel.

theorem HCPolySupport.cubeEuclideanWspKernel_enorm_rpow {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : ‖cubeEuclideanWspKernel s p F z‖ₑ ^ p.exponent.toReal = ENNReal.ofReal (euclideanDist z.1 z.2 ^ (-(↑s * p.exponent.toReal + ↑d))) * ENNReal.ofReal (euclideanNorm (F z.1 - F z.2) ^ p.exponent.toReal)

Exact powered-kernel identity for the Euclidean-distance vector kernel.

theorem HCPolySupport.cubeEuclideanWspKernel_rpow_le_ambientHilbert {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : ‖cubeEuclideanWspKernel s p F z‖ₑ ^ p.exponent.toReal ≤ ‖cubeAmbientHilbertWspKernel s p F z‖ₑ ^ p.exponent.toReal

Pointwise, replacing the Euclidean distance by the ambient distance can only increase the powered kernel.

theorem HCPolySupport.ambientHilbertWspKernel_rpow_le_metric_factor_mul_euclidean {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (z : Vec d × Vec d) : ‖cubeAmbientHilbertWspKernel s p F z‖ₑ ^ p.exponent.toReal ≤ ENNReal.ofReal (↑d ^ (↑s * p.exponent.toReal + ↑d)) * ‖cubeEuclideanWspKernel s p F z‖ₑ ^ p.exponent.toReal

Pointwise reverse metric comparison, before replacing its s-dependent factor by the uniform finite-p factor.

noncomputable def HCPolySupport.cubeCoordinateGagliardoPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : ENNReal

The coordinate scalar Gagliardo energies, each raised to the exact finite p power before summation.

Equations

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

theorem HCPolySupport.cubeCoordinateGagliardoPowerEnergy_eq_lintegral_sum {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : Measurable F) : cubeCoordinateGagliardoPowerEnergy Q s p F = ∫⁻ (z : Vec d × Vec d), ∑ i : Fin d, ‖Gagliardo.gagliardoKernel (↑s) p.exponent (fun (x : Vec d) => F x i) z‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q

The finite coordinate energy is one product-measure integral of the sum of the powered scalar kernels.

theorem HCPolySupport.cubeEuclideanWspESeminorm_rpow_eq_lintegral {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeEuclideanWspESeminorm Q s p F ^ p.exponent.toReal = ∫⁻ (z : Vec d × Vec d), ‖cubeEuclideanWspKernel s p F z‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q

The powered Euclidean seminorm is exactly its kernel integral.

theorem HCPolySupport.cubeAmbientHilbertWspESeminorm_rpow_eq_lintegral {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeAmbientHilbertWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeAmbientHilbertWspESeminorm Q s p F ^ p.exponent.toReal = ∫⁻ (z : Vec d × Vec d), ‖cubeAmbientHilbertWspKernel s p F z‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q

The powered intermediate seminorm is exactly its kernel integral.

theorem HCPolySupport.cubeEuclideanWspESeminorm_rpow_le_ambientHilbert {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeEuclideanWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeEuclideanWspESeminorm Q s p F ^ p.exponent.toReal ≤ cubeAmbientHilbertWspESeminorm Q s p F ^ p.exponent.toReal

Powered Euclidean fractional energy is bounded by the intermediate ambient-distance Hilbert energy.

noncomputable def HCPolySupport.cubeEuclideanWspMetricComparisonConstant (d : ℕ) (p : FiniteLpExponent) : ENNReal

The uniform metric factor for the reverse comparison. It depends only on the dimension and finite exponent, never on s.

Equations

• HCPolySupport.cubeEuclideanWspMetricComparisonConstant d p = ENNReal.ofReal (↑d ^ (↑d + p.exponent.toReal))

theorem HCPolySupport.cubeEuclideanWspMetricComparisonConstant_lt_top (d : ℕ) (p : FiniteLpExponent) : cubeEuclideanWspMetricComparisonConstant d p < ⊤

theorem HCPolySupport.cubeAmbientHilbertWspESeminorm_rpow_le_metricComparisonConstant_mul {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable (cubeAmbientHilbertWspKernel s p F) (Gagliardo.gagliardoCubeMeasure Q)) : cubeAmbientHilbertWspESeminorm Q s p F ^ p.exponent.toReal ≤ cubeEuclideanWspMetricComparisonConstant d p * cubeEuclideanWspESeminorm Q s p F ^ p.exponent.toReal

The intermediate ambient-distance energy is bounded by the Euclidean energy with an explicit constant uniform in the fractional order.

theorem HCPolySupport.cubeCoordinateGagliardoPowerEnergy_le_dimension_mul_ambientHilbert {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : cubeCoordinateGagliardoPowerEnergy Q s p F ≤ ↑d * cubeAmbientHilbertWspESeminorm Q s p F ^ p.exponent.toReal

The sum of scalar coordinate Gagliardo p-energies is controlled by the intermediate Hilbert-vector energy.

noncomputable def HCPolySupport.cubeCoordinateGagliardoComparisonConstant (d : ℕ) (p : FiniteLpExponent) : ENNReal

The explicit finite-dimensional coordinate factor in the reverse Hilbert-vector comparison.

Equations

• HCPolySupport.cubeCoordinateGagliardoComparisonConstant d p = ‖↑d‖ₑ ^ p.exponent.toReal * ↑d ^ (p.exponent.toReal - 1)

theorem HCPolySupport.cubeCoordinateGagliardoComparisonConstant_lt_top (d : ℕ) (p : FiniteLpExponent) : cubeCoordinateGagliardoComparisonConstant d p < ⊤

theorem HCPolySupport.cubeAmbientHilbertWspESeminorm_rpow_le_coordinateGagliardoPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (hF : Measurable F) : cubeAmbientHilbertWspESeminorm Q s p F ^ p.exponent.toReal ≤ cubeCoordinateGagliardoComparisonConstant d p * cubeCoordinateGagliardoPowerEnergy Q s p F

The intermediate Hilbert-vector p-energy is bounded by the finite sum of scalar coordinate Gagliardo energies.