Coarse-graining support: #
Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.QuotientHessianRiesz
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
noncomputable def
HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianRieszRep
{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)
:
↥(ScalarL2 (scaledOpenCubeSet Q ρ₁))
Riesz representative of the open-inner quotient-Hessian functional.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.WeakPoissonEquationOn.inner_openCubeInnerOpenCubeQuotientHessianRieszRep_eq_functional
{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 : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁)))
:
inner ℝ
(h.openCubeInnerOpenCubeQuotientHessianRieszRep hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one
hσ₂_nonneg hσ₂_lt_one hstep_abs)
x = (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
The Riesz representative evaluates against any open-inner L² test as the
continuous quotient-Hessian functional.
theorem
HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianFunctional_apply_subtype
{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 : ↥(h1WeakTestScalarL2Submodule (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)
((h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)).subtype x) = (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
On the dense smooth-test submodule, the continuous open-inner functional agrees with the concrete quotient-Hessian pairing.
theorem
HCPolySupport.WeakPoissonEquationOn.openCubeInnerQuotientHessianSmoothTestBound_nonneg
{d : ℕ}
{Q : TriadicCube d}
(uQ : H1Function (openCubeSet Q))
(f : Vec d → ℝ)
(i : Fin d)
{ρ₁ ρ₂ σ₁ σ₂ : ℝ}
(θ : QuantitativeCubeCutoff Q σ₁ σ₂)
:
The explicit square-root bound used for the quotient-Hessian functional is nonnegative.
theorem
HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeQuotientHessianRieszRep_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 ≤ ρ₁)
:
‖h.openCubeInnerOpenCubeQuotientHessianRieszRep hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one
hσ₂_nonneg hσ₂_lt_one hstep_abs‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ
The Riesz representative has the same explicit norm bound as the continuous open-inner quotient-Hessian functional.
theorem
HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianRieszRep_hasWeakPartialDerivOn_forwardDifferenceQuotient
{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 ≤ ρ₁)
:
HasWeakPartialDerivOn (scaledOpenCubeSet Q ρ₁) j (euclideanForwardDifferenceQuotient step i uQ.toFun) fun (x : Vec d) =>
↑↑(h.openCubeInnerOpenCubeQuotientHessianRieszRep hf hV hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one
hσ₂_nonneg hσ₂_lt_one hstep_abs)
x
For each nonzero step, the Riesz representative is the weak derivative of the forward difference quotient on the open inner cube.