Coarse-graining support: Support.Sobolev.W1p.FiniteMeasureDowngrade

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

Finite-measure downgrades from H¹ to W^{1,p}

On a finite-measure domain, the L² value and weak-gradient data carried by an H1Function also provide W^{1,p} data at every finite exponent p ≤ 2. The analogous conversion for H10Function preserves its smooth, compactly supported approximating sequence and therefore its zero-trace witness.

noncomputable def HCPolySupport.H1Function.toW1pOfExponentLETwo {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H1Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : W1pFunction U p.exponent

Regard an H¹ witness on a finite-measure domain as a W^{1,p} witness whenever p ≤ 2. The value and weak-gradient representatives are unchanged.

Equations

• u.toW1pOfExponentLETwo p hp = { toFun := u.toFun, grad := u.grad, memLp := ⋯, gradMemLp := ⋯, hasWeakGradient := ⋯ }

@[simp]

theorem HCPolySupport.H1Function.toW1pOfExponentLETwo_toFun {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H1Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : (u.toW1pOfExponentLETwo p hp).toFun = u.toFun

@[simp]

theorem HCPolySupport.H1Function.toW1pOfExponentLETwo_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H1Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : (u.toW1pOfExponentLETwo p hp).grad = u.grad

theorem HCPolySupport.H10Function.tendsto_eLpNorm_downgrade_of_two {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] {p : FiniteLpExponent} (hp : p.exponent ≤ 2) {F : ℕ → Vec d → ℝ} {f : Vec d → ℝ} (hF2 : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 (MeasureTheory.volume.restrict U)) (hf2 : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict U)) (hTendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - f x) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - f x) p.exponent (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)

noncomputable def HCPolySupport.H10Function.toW10pOfExponentLETwo {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H10Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : W10pFunction U p.exponent

Regard an H¹₀ witness on a finite-measure domain as a zero-trace W^{1,p} witness whenever p ≤ 2. The value, weak-gradient, and smooth compactly supported approximation representatives are unchanged.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.toW10pOfExponentLETwo_toFun {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H10Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : (u.toW10pOfExponentLETwo p hp).toFun = u.toFun

@[simp]

theorem HCPolySupport.H10Function.toW10pOfExponentLETwo_grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] (u : H10Function U) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : (u.toW10pOfExponentLETwo p hp).grad = u.grad

theorem HCPolySupport.eLpNorm_finiteMeasure_downgrade_le {d : ℕ} {U : Set (Vec d)} (p : FiniteLpExponent) (hp : p.exponent ≤ 2) (f : Vec d → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict U)) : MeasureTheory.eLpNorm f p.exponent (MeasureTheory.volume.restrict U) ≤ MeasureTheory.eLpNorm f 2 (MeasureTheory.volume.restrict U) * (MeasureTheory.volume.restrict U) Set.univ ^ (1 / p.exponent.toReal - 1 / ENNReal.toReal 2)

The finite-measure comparison from a lower finite exponent to L².

theorem HCPolySupport.eLpNorm_normalizedCubeMeasure_downgrade_le {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) (f : Vec d → ℝ) (_hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm f p.exponent (normalizedCubeMeasure Q) ≤ MeasureTheory.eLpNorm f 2 (normalizedCubeMeasure Q)

On a normalized cube, lowering an exponent from 2 costs no measure factor because the normalized cube measure is a probability measure.

theorem HCPolySupport.H1Function.eLpNorm_normalizedCubeMeasure_downgrade_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : MeasureTheory.eLpNorm u.toFun p.exponent (normalizedCubeMeasure Q) ≤ MeasureTheory.eLpNorm u.toFun 2 (normalizedCubeMeasure Q)

The normalized-cube exponent downgrade for the value representative of an H¹ function.

theorem HCPolySupport.H1Function.grad_eLpNorm_normalizedCubeMeasure_downgrade_le {d : ℕ} (Q : TriadicCube d) (u : H1Function (openCubeSet Q)) (i : Fin d) (p : FiniteLpExponent) (hp : p.exponent ≤ 2) : MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p.exponent (normalizedCubeMeasure Q) ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure Q)

The normalized-cube exponent downgrade for a gradient coordinate of an H¹ function.