Coarse-graining support: #
Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.OpenInnerFunctional
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.WeakPoissonEquationOn.integral_norm_sq_h1WeakTest_scaledClosedCubeSet_eq_scaledOpenCubeSet
{d : ℕ}
(Q : TriadicCube d)
(ρ₁ : ℝ)
(φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁))
:
A smooth weak test supported in the open inner cube has the same squared
L² integral over the corresponding closed inner cube.
theorem
HCPolySupport.WeakPoissonEquationOn.integral_norm_sq_sub_h1WeakTest_scaledClosedCubeSet_eq_scaledOpenCubeSet
{d : ℕ}
(Q : TriadicCube d)
(ρ₁ : ℝ)
(φ ψ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁))
:
The squared distance between two open-inner smooth weak tests has the same integral over the corresponding closed inner cube.
theorem
HCPolySupport.WeakPoissonEquationOn.neg_integral_forwardDifference_mul_derivative_openCube_innerOpenCube_eq
{d : ℕ}
{V : Set (Vec d)}
{Q : TriadicCube d}
{uQ : H1Function (openCubeSet Q)}
{f : Vec d → ℝ}
(h : WeakPoissonEquationOn (openCubeSet Q) uQ f)
(hf : MemScalarL2 (openCubeSet Q) f)
(hV : IsOpenBoundedConvexDomain V)
{step : ℝ}
(hstep : step ≠ 0)
(i j : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet Q ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν ≤ σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q)
(φ ψ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁))
(hφψ : φ.toScalarL2 = ψ.toScalarL2)
:
The quotient-Hessian pairing depends only on the open-inner scalar L²
class of a smooth weak test.
noncomputable def
HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianSmoothTestFunctional
{d : ℕ}
{V : Set (Vec d)}
{Q : TriadicCube d}
{uQ : H1Function (openCubeSet Q)}
{f : Vec d → ℝ}
(h : WeakPoissonEquationOn (openCubeSet Q) uQ f)
(hf : MemScalarL2 (openCubeSet Q) f)
(hV : IsOpenBoundedConvexDomain V)
{step : ℝ}
(hstep : step ≠ 0)
(i j : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet Q ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν ≤ σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q)
:
The concrete quotient-Hessian pairing on the dense smooth-test submodule
over the open inner cube. The estimates are still supplied by the closed
inner cube, using scaledOpenCubeSet_subset_scaledClosedCubeSet.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeQuotientHessianSmoothTestFunctional_apply_le
{d : ℕ}
{V : Set (Vec d)}
{Q : TriadicCube d}
{uQ : H1Function (openCubeSet Q)}
{f : Vec d → ℝ}
(h : WeakPoissonEquationOn (openCubeSet Q) uQ f)
(hf : MemScalarL2 (openCubeSet Q) f)
(hV : IsOpenBoundedConvexDomain V)
{step : ℝ}
(hstep : step ≠ 0)
(i j : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet Q ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν ≤ σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q)
(x : ↥(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)))
:
‖(h.openCubeInnerOpenCubeQuotientHessianSmoothTestFunctional hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ
hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs)
x‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ * ‖(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)).subtype x‖
The open-inner smooth-test functional satisfies the closed-inner square-root operator bound.
noncomputable def
HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianFunctional
{d : ℕ}
{V : Set (Vec d)}
{Q : TriadicCube d}
{uQ : H1Function (openCubeSet Q)}
{f : Vec d → ℝ}
(h : WeakPoissonEquationOn (openCubeSet Q) uQ f)
(hf : MemScalarL2 (openCubeSet Q) f)
(hV : IsOpenBoundedConvexDomain V)
{step : ℝ}
(hstep : step ≠ 0)
(i j : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet Q ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν ≤ σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q)
:
Continuous extension of the open-inner quotient-Hessian functional from
smooth tests to all scalar L² fields on the open inner cube.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeQuotientHessianFunctional_apply_le
{d : ℕ}
{V : Set (Vec d)}
{Q : TriadicCube d}
{uQ : H1Function (openCubeSet Q)}
{f : Vec d → ℝ}
(h : WeakPoissonEquationOn (openCubeSet Q) uQ f)
(hf : MemScalarL2 (openCubeSet Q) f)
(hV : IsOpenBoundedConvexDomain V)
{step : ℝ}
(hstep : step ≠ 0)
(i j : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ ν : ℝ}
(η : QuantitativeCubeCutoff Q ρ₁ ρ₂)
(hη_sub : tsupport η.toFun ⊆ V)
(hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V)
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
(hVν : V ⊆ scaledClosedCubeSet Q ν)
(hν_nonneg : 0 ≤ ν)
(hνσ : ν ≤ σ₁)
(hσ₁_lt_one : σ₁ < 1)
(hσ₂_nonneg : 0 ≤ σ₂)
(hσ₂_lt_one : σ₂ < 1)
(hstep_abs : |step| ≤ (σ₁ - ν) * cubeRadius Q)
(hρ₁_nonneg : 0 ≤ ρ₁)
(x : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁)))
:
‖(h.openCubeInnerOpenCubeQuotientHessianFunctional hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one
hσ₂_nonneg hσ₂_lt_one hstep_abs)
x‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ * ‖x‖
The continuous open-inner quotient-Hessian functional inherits the same explicit bound as the dense smooth-test functional.