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

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

Diagonal convex smoothing of fractional kernels

The inward convex smoother acts on a fractional difference quotient by sampling both variables with the same affine map. This module records that operator separately from the source-facing fractional Sobolev API. Its measure estimates are the analytic input for smooth density on cubes.

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

Apply one inward affine sample map simultaneously to both arguments of a fractional kernel.

Equations

• HCPolySupport.diagonalConvexApproxSample x0 z r ε xy = (HCPolySupport.convexApproxSample x0 z r ε xy.1, HCPolySupport.convexApproxSample x0 z r ε xy.2)

@[simp]

theorem HCPolySupport.diagonalConvexApproxSample_apply {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (xy : Vec d × Vec d) : diagonalConvexApproxSample x0 z r ε xy = (convexApproxSample x0 z r ε xy.1, convexApproxSample x0 z r ε xy.2)

noncomputable def HCPolySupport.diagonalConvexApproxAverage {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ρ : Vec d → ℝ) (H : Vec d × Vec d → E) (x0 : Vec d) (r ε : ℝ) (xy : Vec d × Vec d) : E

Average a vector-valued Gagliardo kernel along the diagonal inward affine samples. This is deliberately an internal analytic operator, not a new fractional-Sobolev norm.

Equations

• HCPolySupport.diagonalConvexApproxAverage ρ H x0 r ε xy = ∫ (z : HCPolySupport.Vec d) in tsupport ρ, ρ z • H (HCPolySupport.diagonalConvexApproxSample x0 z r ε xy)

noncomputable def HCPolySupport.convexApproxKernelMeasure {d : ℕ} (ρ : Vec d → ℝ) : MeasureTheory.Measure (Vec d)

The probability measure associated with a nonnegative unit-mass convex approximation kernel.

Equations

• HCPolySupport.convexApproxKernelMeasure ρ = MeasureTheory.volume.withDensity fun (z : HCPolySupport.Vec d) => ENNReal.ofReal (ρ z)

theorem HCPolySupport.isProbabilityMeasure_convexApproxKernelMeasure {d : ℕ} {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) : MeasureTheory.IsProbabilityMeasure (convexApproxKernelMeasure ρ)

@[simp]

theorem HCPolySupport.diagonalConvexApproxAverage_apply {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (ρ : Vec d → ℝ) (H : Vec d × Vec d → E) (x0 : Vec d) (r ε : ℝ) (xy : Vec d × Vec d) : diagonalConvexApproxAverage ρ H x0 r ε xy = ∫ (z : Vec d) in tsupport ρ, ρ z • H (diagonalConvexApproxSample x0 z r ε xy)

theorem HCPolySupport.setIntegral_smul_eq_integral_convexApproxKernelMeasure {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (G : Vec d → E) : ∫ (z : Vec d) in tsupport ρ, ρ z • G z = ∫ (z : Vec d), G z ∂convexApproxKernelMeasure ρ

Recast a kernel-weighted set integral as a Bochner integral against the probability measure carried by the smoothing kernel.

theorem HCPolySupport.diagonalConvexApproxAverage_eq_integral_kernelMeasure {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (H : Vec d × Vec d → E) (x0 : Vec d) (r ε : ℝ) (xy : Vec d × Vec d) : diagonalConvexApproxAverage ρ H x0 r ε xy = ∫ (z : Vec d), H (diagonalConvexApproxSample x0 z r ε xy) ∂convexApproxKernelMeasure ρ

Recast the diagonal average as a Bochner integral against the probability measure carried by the smoothing kernel.

theorem HCPolySupport.euclideanDist_convexApproxSample {d : ℕ} (x0 z : Vec d) (r ε : ℝ) (hε : ε < 1) (x y : Vec d) : euclideanDist (convexApproxSample x0 z r ε x) (convexApproxSample x0 z r ε y) = (1 - ε) * euclideanDist x y

The simultaneous affine sampling map contracts Euclidean pair distances by the scalar factor 1 - ε.

theorem HCPolySupport.cubeEuclideanWspKernel_comp_diagonalConvexApproxSample {d : ℕ} (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) (x0 z : Vec d) (r ε : ℝ) (hε : ε < 1) (xy : Vec d × Vec d) : cubeEuclideanWspKernel s p (fun (x : Vec d) => F (convexApproxSample x0 z r ε x)) xy = (1 - ε) ^ (↑s + ↑d / p.exponent.toReal) • cubeEuclideanWspKernel s p F (diagonalConvexApproxSample x0 z r ε xy)

Pulling a Euclidean fractional kernel through one diagonal affine sample has the exact scaling dictated by the fractional order.

theorem HCPolySupport.map_prod_restrict_diagonalConvexApproxSample {d : ℕ} {U : Set (Vec d)} (hU : MeasurableSet U) (x0 z : Vec d) (r ε : ℝ) (hε : ε < 1) : MeasureTheory.Measure.map (diagonalConvexApproxSample x0 z r ε) ((MeasureTheory.volume.restrict U).prod (MeasureTheory.volume.restrict U)) = ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2 • (MeasureTheory.volume.restrict (convexApproxSample x0 z r ε '' U)).prod (MeasureTheory.volume.restrict (convexApproxSample x0 z r ε '' U))

The diagonal affine sampling map transports a product of restricted volume measures with one Jacobian factor for each cube variable.

theorem HCPolySupport.map_gagliardoCubeMeasure_diagonalConvexApproxSample {d : ℕ} (Q : TriadicCube d) (x0 z : Vec d) (r ε : ℝ) (hε : ε < 1) : MeasureTheory.Measure.map (diagonalConvexApproxSample x0 z r ε) (Gagliardo.gagliardoCubeMeasure Q) = ENNReal.ofReal (cubeVolume Q)⁻¹ • ENNReal.ofReal ((1 - ε) ^ d)⁻¹ ^ 2 • (MeasureTheory.volume.restrict (convexApproxSample x0 z r ε '' cubeSet Q)).prod (MeasureTheory.volume.restrict (convexApproxSample x0 z r ε '' cubeSet Q))

The corresponding transport formula for the normalized-first-variable Gagliardo measure. The cube normalization is unchanged; the two affine Jacobians are explicit.

theorem HCPolySupport.convexOn_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {q : ℝ} (hq : 1 ≤ q) : ConvexOn ℝ Set.univ fun (v : E) => ‖v‖ ^ q

The p-th power of the norm is convex for the finite exponents used by the fractional theory.

theorem HCPolySupport.lintegral_enorm_rpow_integral_le_lintegral_lintegral {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β) [MeasureTheory.SFinite μ] [MeasureTheory.IsProbabilityMeasure ν] {H : β → α → E} {q : ℝ} (hq : 1 ≤ q) (hsection : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (z : β) => H z x) ν) (hsectionpow : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (z : β) => ‖H z x‖ ^ q) ν) (hpow_meas : AEMeasurable (fun (xz : α × β) => ‖H xz.2 xz.1‖ₑ ^ q) (μ.prod ν)) : ∫⁻ (x : α), ‖∫ (z : β), H z x ∂ν‖ₑ ^ q ∂μ ≤ ∫⁻ (z : β), ∫⁻ (x : α), ‖H z x‖ₑ ^ q ∂μ ∂ν

Pointwise vector Jensen followed by Tonelli. The averaging variable is kept scalar, which avoids any measurable Lp-valued section construction. This is the finite-p estimate used by diagonal Gagliardo averaging.

theorem HCPolySupport.lintegral_convexApproxKernelAverage_rpow_le {d : ℕ} {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (H : Vec d → α → E) {q : ℝ} (hq : 1 ≤ q) (hsection : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (z : Vec d) => H z x) (convexApproxKernelMeasure ρ)) (hsectionpow : ∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (z : Vec d) => ‖H z x‖ ^ q) (convexApproxKernelMeasure ρ)) (hpow_meas : AEMeasurable (fun (xz : α × Vec d) => ‖H xz.2 xz.1‖ₑ ^ q) (μ.prod (convexApproxKernelMeasure ρ))) : ∫⁻ (x : α), ‖∫ (z : Vec d) in tsupport ρ, ρ z • H z x‖ₑ ^ q ∂μ ≤ ∫⁻ (z : Vec d), ∫⁻ (x : α), ‖H z x‖ₑ ^ q ∂μ ∂convexApproxKernelMeasure ρ

Powered L^p control of an average against the convex kernel measure. The three section hypotheses are analytic integrability obligations; later transport lemmas discharge them from MemLp of a Gagliardo kernel.

theorem HCPolySupport.lintegral_diagonalConvexApproxAverage_rpow_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure (Vec d × Vec d)) [MeasureTheory.SFinite μ] {ρ : Vec d → ℝ} (hρ : IsConvexApproxKernel ρ) (K : Vec d × Vec d → E) (x0 : Vec d) (r ε : ℝ) {q : ℝ} (hq : 1 ≤ q) (hsection : ∀ᵐ (xy : Vec d × Vec d) ∂μ, MeasureTheory.Integrable (fun (z : Vec d) => K (diagonalConvexApproxSample x0 z r ε xy)) (convexApproxKernelMeasure ρ)) (hsectionpow : ∀ᵐ (xy : Vec d × Vec d) ∂μ, MeasureTheory.Integrable (fun (z : Vec d) => ‖K (diagonalConvexApproxSample x0 z r ε xy)‖ ^ q) (convexApproxKernelMeasure ρ)) (hpow_meas : AEMeasurable (fun (xyz : (Vec d × Vec d) × Vec d) => ‖K (diagonalConvexApproxSample x0 xyz.2 r ε xyz.1)‖ₑ ^ q) (μ.prod (convexApproxKernelMeasure ρ))) : ∫⁻ (xy : Vec d × Vec d), ‖diagonalConvexApproxAverage ρ K x0 r ε xy‖ₑ ^ q ∂μ ≤ ∫⁻ (z : Vec d), ∫⁻ (xy : Vec d × Vec d), ‖K (diagonalConvexApproxSample x0 z r ε xy)‖ₑ ^ q ∂μ ∂convexApproxKernelMeasure ρ

The preceding Jensen--Tonelli estimate specialized to diagonal affine sampling of a fractional kernel.