EnergyDuality

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Centered-cube Neumann energy and duality

This file supplies the q = 2 energy endpoint and the canonical mean-zero adjoint used by the below-two Neumann Calderón--Zygmund argument. Coercivity and solvability are discharged internally from the centered-cube geometry.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeH1MeanZeroScalarDivergence_cz_two {d : ℕ} (m : ℤ) (sigma0 : ℝ) (h : CubeEuclideanLpField (originCube d m) FiniteLpExponent.two) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (hsigma0 : 0 < sigma0) (hsolution : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h.toField x) : (centeredCubeDomain d m).normalizedEuclideanLpENorm FiniteLpExponent.two.exponent u.toH1Function.grad ≤ (ENNReal.ofReal sigma0)⁻¹ * (centeredCubeDomain d m).normalizedEuclideanLpENorm FiniteLpExponent.two.exponent h.toField

The q = 2 energy estimate for a supplied mean-zero Neumann solution on a centered cube. The datum is only the normalized Euclidean L² field exposed by the finite-exponent API.

theorem HCPolySupport.CubeCalderonZygmund.nonempty_openCubeSet_originCube_neumann (d : ℕ) (m : ℤ) : (openCubeSet (originCube d m)).Nonempty

theorem HCPolySupport.CubeCalderonZygmund.isEllipticFieldOn_scalarMatrix_centeredCube {d : ℕ} {m : ℤ} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) : IsEllipticFieldOn sigma0 sigma0 (openCubeSet (originCube d m)) fun (x : Vec d) => scalarMatrix sigma0

noncomputable def HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergenceSolution {d : ℕ} (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : H1MeanZeroFunction (openCubeSet (originCube d m))

The canonical mean-zero solution of the scalar divergence equation with datum -G on a centered cube.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergenceSolution_isWeakSolution {d : ℕ} (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) (centeredCubeMeanZeroScalarDivergenceSolution m hsigma0 G hG) fun (x : Vec d) => -G x

The canonical mean-zero adjoint satisfies the packaged weak equation with the same negative-datum convention as the supplied solution.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergenceSolution_weak {d : ℕ} (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) (psi : H1MeanZeroFunction (openCubeSet (originCube d m))) : sigma0 * ∫ (x : Vec d) in openCubeSet (originCube d m), vecDot ((centeredCubeMeanZeroScalarDivergenceSolution m hsigma0 G hG).toH1Function.grad x) (psi.toH1Function.grad x) = -∫ (x : Vec d) in openCubeSet (originCube d m), vecDot (G x) (psi.toH1Function.grad x)

Raw-volume weak equation for the canonical centered Neumann adjoint.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergenceSolution_normalized_weak {d : ℕ} (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) (psi : H1MeanZeroFunction (openCubeSet (originCube d m))) : sigma0 * ∫ (x : Vec d), vecDot ((centeredCubeMeanZeroScalarDivergenceSolution m hsigma0 G hG).toH1Function.grad x) (psi.toH1Function.grad x) ∂(centeredCubeDomain d m).normalizedVolume = -∫ (x : Vec d), vecDot (G x) (psi.toH1Function.grad x) ∂(centeredCubeDomain d m).normalizedVolume

Normalized-volume weak equation for the canonical centered Neumann adjoint.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergence_cross_pairing {d : ℕ} (m : ℤ) {sigma0 : ℝ} (u v : H1MeanZeroFunction (openCubeSet (originCube d m))) (h G : Vec d → Vec d) (hu : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h x) (hv : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) v fun (x : Vec d) => -G x) : ∫ (x : Vec d), vecDot (u.toH1Function.grad x) (G x) ∂(centeredCubeDomain d m).normalizedVolume = ∫ (x : Vec d), vecDot (h x) (v.toH1Function.grad x) ∂(centeredCubeDomain d m).normalizedVolume

Exact normalized cross-pairing identity for two supplied centered Neumann scalar-divergence solutions.

theorem HCPolySupport.CubeCalderonZygmund.centeredCubeMeanZeroScalarDivergenceSolution_normalized_cross_pairing {d : ℕ} (m : ℤ) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (h G : Vec d → Vec d) (hu : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => scalarMatrix sigma0) (openCubeSet (originCube d m)) u fun (x : Vec d) => -h x) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ∫ (x : Vec d), vecDot (u.toH1Function.grad x) (G x) ∂(centeredCubeDomain d m).normalizedVolume = ∫ (x : Vec d), vecDot (h x) ((centeredCubeMeanZeroScalarDivergenceSolution m hsigma0 G hG).toH1Function.grad x) ∂(centeredCubeDomain d m).normalizedVolume

Cross-pair a supplied centered Neumann solution against the canonical mean-zero adjoint.