Coarse-graining support: Support.Sobolev.Foundations.CoerciveH10

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

noncomputable def HCPolySupport.H10Function.approxH1 {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) (n : ℕ) : H1Function U

Package an H¹₀ function's nth smooth compactly supported approximation as an H¹ function on an open domain.

Equations

• HCPolySupport.H10Function.approxH1 hU u n = HCPolySupport.H1Function.ofContDiff hU ⋯ ⋯

theorem HCPolySupport.H10Function.approx_memL2_sub_toH1_memL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) (n : ℕ) : MeasureTheory.MemLp (fun (x : Vec d) => u.approx n x - u.toFun x) 2 (volumeMeasureOn U)

theorem HCPolySupport.H10Function.approx_grad_memL2_sub_toH1_grad_memL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) (n : ℕ) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ (u.approx n) x) (basisVec i) - u.grad x i) 2 (volumeMeasureOn U)

theorem HCPolySupport.H10Function.tendsto_approxH1_toScalarL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) : Filter.Tendsto (fun (n : ℕ) => (approxH1 hU u n).toScalarL2) Filter.atTop (nhds u.toScalarL2)

theorem HCPolySupport.H10Function.tendsto_approxH1_gradCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) (i : Fin d) : Filter.Tendsto (fun (n : ℕ) => (approxH1 hU u n).gradCoordToScalarL2 i) Filter.atTop (nhds (u.gradCoordToScalarL2 i))

theorem HCPolySupport.H10Function.tendsto_approxH1_gradientCoordL2NormSum {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) (u : H10Function U) : Filter.Tendsto (fun (n : ℕ) => (approxH1 hU u n).gradientCoordL2NormSum) Filter.atTop (nhds u.gradientCoordL2NormSum)

theorem HCPolySupport.H10Function.valueL2Norm_le_sobolevConst_mul_gradientCoordL2NormSum_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hd : 2 < d) (u : H10Function U) : ‖u.toScalarL2‖ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ MeasureTheory.volume U 2 2) * u.gradientCoordL2NormSum

On bounded open convex domains, the H¹₀ approximation package yields the coercive estimate proved for smooth compactly supported functions in dimensions d ≥ 3.

theorem HCPolySupport.H10Function.valueL2Norm_le_sobolevConst_mul_gradientL2Norm_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hd : 2 < d) (u : H10Function U) : ‖u.toScalarL2‖ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst ℝ MeasureTheory.volume U 2 2) * ↑d * ‖u.gradToVectorL2‖

A coarser but more directly typed H¹₀ coercive estimate, obtained by bounding the coordinate-gradient sum by the repo's existing vector L² norm.

theorem HCPolySupport.H10Function.toScalarL2_eq_zero_of_gradToVectorL2_eq_zero_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hd : 2 < d) (u : H10Function U) (hgrad : u.gradToVectorL2 = 0) : u.toScalarL2 = 0

On a bounded open convex domain, an H¹₀ function with zero gradient L² class has zero value L² class.

theorem HCPolySupport.H10Function.toScalarL2_eq_zero_of_grad_eq_zero_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hd : 2 < d) (u : H10Function U) (hgrad : u.grad = 0) : u.toScalarL2 = 0

On a bounded open convex domain, an H¹₀ function with zero weak gradient has zero value L² class.

theorem HCPolySupport.H10Function.exists_valueL2_bound_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (hd : 2 < d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : H10Function U), ‖u.toScalarL2‖ ≤ C * u.gradientCoordL2NormSum

Existential constant form of the bounded-open-convex H¹₀ coercive estimate in dimensions d ≥ 3.