Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.LimitHessian

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

Limiting Hessian functional

This file isolates the final compactness/limit handoff for the interior difference-quotient proof. The hypothesis is deliberately narrow: for a small-step sequence, the already-built quotient Hessian pairings converge on smooth tests to the desired pairing against uQ.grad. From that hypothesis and the uniform quotient estimate, we build the bounded limiting functional.

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeQuotientHessianPairing {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (V : Set (Vec d)) (step : ℝ) (i j : Fin d) {ρ₁ : ℝ} (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) : ℝ

The concrete fixed-step quotient-Hessian pairing on a smooth open-inner test.

Equations

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

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianPairing {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (V : Set (Vec d)) (i j : Fin d) {ρ₁ : ℝ} (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) : ℝ

The limiting Hessian pairing on a smooth open-inner test.

Equations

• HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianPairing uQ V i j φ = -∫ (x : HCPolySupport.Vec d) in V, uQ.grad x i * (fderiv ℝ φ.toFun x) (HCPolySupport.basisVec j)

def HCPolySupport.WeakPoissonEquationOn.OpenCubeInnerHessianPairingTendsto {d : ℕ} {Q : TriadicCube d} (uQ : H1Function (openCubeSet Q)) (V : Set (Vec d)) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ : ℝ} : Prop

Smooth-test convergence hypothesis for a fixed sequence of legal difference-quotient steps.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianPairing_eq_of_toScalarL2_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (φ ψ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) (hφψ : φ.toScalarL2 = ψ.toScalarL2) : openCubeInnerOpenCubeLimitHessianPairing uQ V i j φ = openCubeInnerOpenCubeLimitHessianPairing uQ V i j ψ

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianPairing_add {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} (hV : IsOpenBoundedConvexDomain V) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ σ₁ ν : ℝ} (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (φ ψ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) : openCubeInnerOpenCubeLimitHessianPairing uQ V i j (φ.add ψ) = openCubeInnerOpenCubeLimitHessianPairing uQ V i j φ + openCubeInnerOpenCubeLimitHessianPairing uQ V i j ψ

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianPairing_smul {d : ℕ} {V : Set (Vec d)} {Q : TriadicCube d} {uQ : H1Function (openCubeSet Q)} (hV : IsOpenBoundedConvexDomain V) (stepSeq : ℕ → ℝ) (i j : Fin d) {ρ₁ σ₁ ν : ℝ} (hinnerV : scaledClosedCubeSet Q ρ₁ ⊆ V) (hVν : V ⊆ scaledClosedCubeSet Q ν) (hν_nonneg : 0 ≤ ν) (hνσ : ν ≤ σ₁) (hσ₁_lt_one : σ₁ < 1) (hstep_abs : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (c : ℝ) (φ : H1WeakTestFunction (scaledOpenCubeSet Q ρ₁)) : openCubeInnerOpenCubeLimitHessianPairing uQ V i j (H1WeakTestFunction.smul c φ) = c * openCubeInnerOpenCubeLimitHessianPairing uQ V i j φ

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianSmoothTestFunctional {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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) : ↥(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)) →ₗ[ℝ] ℝ

The limiting Hessian pairing as a linear functional on the dense smooth-test scalar L² submodule.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeLimitHessianSmoothTestFunctional_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (x : ↥(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁))) : ‖(h.openCubeInnerOpenCubeLimitHessianSmoothTestFunctional hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ * ‖(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)).subtype x‖

The limiting smooth-test functional inherits the uniform quotient-Hessian bound.

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianFunctional {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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁)) →L[ℝ] ℝ

Continuous extension of the limiting Hessian functional to all scalar L² fields on the open inner cube.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeLimitHessianFunctional_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (hρ₁_nonneg : 0 ≤ ρ₁) (x : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁))) : ‖(h.openCubeInnerOpenCubeLimitHessianFunctional hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ * ‖x‖

The limiting continuous functional inherits the uniform quotient bound.

noncomputable def HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianRieszRep {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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁))

Riesz representative of the limiting open-inner Hessian functional.

Equations

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

theorem HCPolySupport.WeakPoissonEquationOn.inner_openCubeInnerOpenCubeLimitHessianRieszRep_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (x : ↥(ScalarL2 (scaledOpenCubeSet Q ρ₁))) : inner ℝ (h.openCubeInnerOpenCubeLimitHessianRieszRep hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x = (h.openCubeInnerOpenCubeLimitHessianFunctional hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x

Riesz evaluation theorem for the limiting Hessian representative.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianFunctional_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (hρ₁_nonneg : 0 ≤ ρ₁) (x : ↥(h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁))) : (h.openCubeInnerOpenCubeLimitHessianFunctional hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) ((h1WeakTestScalarL2Submodule (scaledOpenCubeSet Q ρ₁)).subtype x) = (h.openCubeInnerOpenCubeLimitHessianSmoothTestFunctional hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x

The continuous limiting functional agrees with the concrete smooth-test functional on the dense submodule.

theorem HCPolySupport.WeakPoissonEquationOn.norm_openCubeInnerOpenCubeLimitHessianRieszRep_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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (hρ₁_nonneg : 0 ≤ ρ₁) : ‖h.openCubeInnerOpenCubeLimitHessianRieszRep hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim‖ ≤ openCubeInnerQuotientHessianSmoothTestBound uQ f i θ

The limiting Riesz representative has the same explicit norm bound as the fixed-step quotient representatives.

theorem HCPolySupport.WeakPoissonEquationOn.openCubeInnerOpenCubeLimitHessianRieszRep_hasWeakPartialDerivOn_grad {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) (stepSeq : ℕ → ℝ) (hstep : ∀ (n : ℕ), stepSeq n ≠ 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 : ∀ (n : ℕ), |stepSeq n| ≤ (σ₁ - ν) * cubeRadius Q) (hlim : OpenCubeInnerHessianPairingTendsto uQ V stepSeq i j) (hρ₁_nonneg : 0 ≤ ρ₁) : HasWeakPartialDerivOn (scaledOpenCubeSet Q ρ₁) j (fun (x : Vec d) => uQ.grad x i) fun (x : Vec d) => ↑↑(h.openCubeInnerOpenCubeLimitHessianRieszRep hf hV stepSeq hstep i j η hη_sub hinnerV θ hVν hν_nonneg hνσ hσ₁_lt_one hσ₂_nonneg hσ₂_lt_one hstep_abs hlim) x

Under the smooth-test pairing convergence hypothesis, the limiting Riesz representative is the weak j-derivative of the ith weak-gradient coordinate on the open inner cube.