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

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

Finite-p bounds for diagonal Gagliardo smoothing

This module begins the measure-transport layer needed to turn the diagonal Jensen estimate into an unconditional fractional-kernel bound.

theorem HCPolySupport.ae_mem_tsupport_convexApproxKernelMeasure {d : ℕ} {ρ : Vec d → ℝ} : ∀ᵐ (z : Vec d) ∂convexApproxKernelMeasure ρ, z ∈ tsupport ρ

The kernel probability measure is concentrated on the topological support of its density.

def HCPolySupport.diagonalConvexApproxJointSample {d : ℕ} (x0 : Vec d) (r ε : ℝ) : (Vec d × Vec d) × Vec d → Vec d × Vec d

The joint map used when Fubini interchanges the cube variables and the kernel variable in diagonal smoothing.

Equations

• HCPolySupport.diagonalConvexApproxJointSample x0 r ε xyz = HCPolySupport.diagonalConvexApproxSample x0 xyz.2 r ε xyz.1

theorem HCPolySupport.measurable_diagonalConvexApproxJointSample {d : ℕ} (x0 : Vec d) (r ε : ℝ) : Measurable (diagonalConvexApproxJointSample x0 r ε)

theorem HCPolySupport.diagonalConvexApproxSample_mapsTo_openCubeProduct {d : ℕ} (Q : TriadicCube d) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 z : Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hz : z ∈ tsupport ρ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : Set.MapsTo (diagonalConvexApproxSample x0 z r ε) (openCubeSet Q ×ˢ openCubeSet Q) (openCubeSet Q ×ˢ openCubeSet Q)

On the support of the convex kernel, simultaneous inward sampling maps the open cube product into itself.

theorem HCPolySupport.map_gagliardoCubeMeasure_diagonalConvexApproxSample_le {d : ℕ} (Q : TriadicCube d) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 z : Vec d} {r ε : ℝ} (hε : ε < 1) (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hz : z ∈ tsupport ρ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : MeasureTheory.Measure.map (diagonalConvexApproxSample x0 z r ε) (Gagliardo.gagliardoCubeMeasure Q) ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2 • Gagliardo.gagliardoCubeMeasure Q

The pushed-forward Gagliardo measure of a fixed supported diagonal sample is bounded by its two-Jacobian factor times the original measure.

theorem HCPolySupport.eLpNorm_comp_diagonalConvexApproxSample_le {d : ℕ} {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (Q : TriadicCube d) (p : FiniteLpExponent) (K : Vec d × Vec d → E) (hK : MeasureTheory.MemLp K p.exponent (Gagliardo.gagliardoCubeMeasure Q)) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 z : Vec d} {r ε : ℝ} (hε : ε < 1) (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hz : z ∈ tsupport ρ) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : MeasureTheory.eLpNorm (fun (xy : Vec d × Vec d) => K (diagonalConvexApproxSample x0 z r ε xy)) p.exponent (Gagliardo.gagliardoCubeMeasure Q) ≤ (ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2) ^ (1 / p.exponent).toReal * MeasureTheory.eLpNorm K p.exponent (Gagliardo.gagliardoCubeMeasure Q)

A fixed supported diagonal affine sample is bounded on finite- L^p Gagliardo kernels by the explicit two-Jacobian factor.

theorem HCPolySupport.map_diagonalConvexApproxJointSample_le {d : ℕ} (Q : TriadicCube d) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 : Vec d} {r ε : ℝ} (hε : ε < 1) (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : MeasureTheory.Measure.map (diagonalConvexApproxJointSample x0 r ε) ((Gagliardo.gagliardoCubeMeasure Q).prod (convexApproxKernelMeasure ρ)) ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2 • Gagliardo.gagliardoCubeMeasure Q

The joint diagonal sampling map is quasi-measure-preserving with exactly the two-Jacobian loss. This is the missing bridge from fixed-sample bounds to Fubini section statements.

theorem HCPolySupport.lintegral_diagonalConvexApproxAverage_rpow_le_of_memLp {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : TriadicCube d) (p : FiniteLpExponent) (K : Vec d × Vec d → E) (hK : MeasureTheory.MemLp K p.exponent (Gagliardo.gagliardoCubeMeasure Q)) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 : Vec d} {r ε : ℝ} (hε : ε < 1) (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : ∫⁻ (xy : Vec d × Vec d), ‖diagonalConvexApproxAverage ρ K x0 r ε xy‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q ≤ ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2 * ∫⁻ (xy : Vec d × Vec d), ‖K xy‖ₑ ^ p.exponent.toReal ∂Gagliardo.gagliardoCubeMeasure Q

The diagonal convex average satisfies the powered finite-L^p Gagliardo bound without caller-supplied Fubini section hypotheses.

theorem HCPolySupport.eLpNorm_diagonalConvexApproxAverage_le_of_memLp {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (Q : TriadicCube d) (p : FiniteLpExponent) (K : Vec d × Vec d → E) (hK : MeasureTheory.MemLp K p.exponent (Gagliardo.gagliardoCubeMeasure Q)) {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) {x0 : Vec d} {r ε : ℝ} (hε : ε < 1) (hball : Metric.closedBall x0 r ⊆ openCubeSet Q) (hr : 0 ≤ r) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : MeasureTheory.eLpNorm (diagonalConvexApproxAverage ρ K x0 r ε) p.exponent (Gagliardo.gagliardoCubeMeasure Q) ≤ (ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2) ^ (1 / p.exponent).toReal * MeasureTheory.eLpNorm K p.exponent (Gagliardo.gagliardoCubeMeasure Q)

The unconditional finite-L^p norm form of the diagonal Gagliardo average bound.