Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.FoldedAndWeakScalar #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.equation_foldedCubeUpperFaceTest
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
:
∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient (foldedCubeUpperFaceTest Q i φ) x) = ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeUpperFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x
The weak Neumann equation tested against the folded upper-face reflection test. This is the formal replacement for saying that the one-face even reflection solves the reflected equation.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.equation_foldedCubeLowerFaceTest
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
:
∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient (foldedCubeLowerFaceTest Q i φ) x) = ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeLowerFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x
The weak Neumann equation tested against the folded lower-face reflection test.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedGradient_pairing_eq_rhs
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hreflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
(∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (W.w.toH1Function.grad (cubeUpperFaceReflection Q i x)))
(euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeUpperFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x
One upper-face weak reflection identity for an arbitrary smooth test. The second integral is over the neighboring reflected cube with the reflected weak gradient field.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedGradient_pairing_eq_rhs
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hreflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
(∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (W.w.toH1Function.grad (cubeLowerFaceReflection Q i x)))
(euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q, F x * (foldedCubeLowerFaceMeanZeroH1Test Q i hφ).toH1Function.toFun x
One lower-face weak reflection identity for an arbitrary smooth test. The second integral is over the neighboring reflected cube with the reflected weak gradient field.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedGradient_pairing_eq_reflectedRhs
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmean : cubeAverage Q F = 0)
(hgradMain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hgradReflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFreflected :
MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeUpperFaceReflection Q i x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
(∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (W.w.toH1Function.grad (cubeUpperFaceReflection Q i x)))
(euclideanGradient φ x) = (∫ (x : Vec d) in openCubeSet Q, F x * φ x) + ∫ (x : Vec d) in openCubeSet (cubeUpperFaceNeighbor Q i), F (cubeUpperFaceReflection Q i x) * φ x
One upper-face reflected weak equation with the forcing also split across the reflected neighboring cube. This is the weak-form version of the reflected solution statement for a zero-average forcing.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedGradient_pairing_eq_reflectedRhs
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmean : cubeAverage Q F = 0)
(hgradMain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hgradReflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFreflected :
MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeLowerFaceReflection Q i x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
(∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x)) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), vecDot ((coordReflectionLinear i) (W.w.toH1Function.grad (cubeLowerFaceReflection Q i x)))
(euclideanGradient φ x) = (∫ (x : Vec d) in openCubeSet Q, F x * φ x) + ∫ (x : Vec d) in openCubeSet (cubeLowerFaceNeighbor Q i), F (cubeLowerFaceReflection Q i x) * φ x
One lower-face reflected weak equation with the forcing also split across the reflected neighboring cube.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedWeakEquationOnUnion
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmean : cubeAverage Q F = 0)
(hgradMain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hgradReflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeUpperFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFreflected :
MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeUpperFaceReflection Q i x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedForcingIntegrand Q i F φ x
Upper-face reflected weak equation written as a single integral over the
doubled open domain Q ∪ Q⁺.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedWeakEquationOnUnion
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hmean : cubeAverage Q F = 0)
(hgradMain :
MeasureTheory.Integrable (fun (x : Vec d) => vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hgradReflected :
MeasureTheory.Integrable
(fun (x : Vec d) =>
vecDot (W.w.toH1Function.grad x) (euclideanGradient (fun (z : Vec d) => φ (cubeLowerFaceReflection Q i z)) x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
(hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFmain : MeasureTheory.Integrable (fun (x : Vec d) => F x * φ x) (MeasureTheory.volume.restrict (openCubeSet Q)))
(hFreflected :
MeasureTheory.Integrable (fun (x : Vec d) => F x * φ (cubeLowerFaceReflection Q i x))
(MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedForcingIntegrand Q i F φ x
Lower-face reflected weak equation written as a single integral over the
doubled open domain Q ∪ Q⁻.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedWeakEquationOnUnion_of_compactSupport
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedForcingIntegrand Q i F φ x
Compact-test version of the upper-face reflected weak equation. This
derives the side integrability assumptions in
upperFace_reflectedWeakEquationOnUnion from the natural L² data.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedWeakEquationOnUnion_of_compactSupport
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedForcingIntegrand Q i F φ x
Compact-test version of the lower-face reflected weak equation. This
derives the side integrability assumptions in
lowerFace_reflectedWeakEquationOnUnion from the natural L² data.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.weakEquationOnCube_of_compactSupport
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q)))
:
∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q, F x * φ x
Compact-test weak equation on the original cube. The test need not be mean-zero: the zero-average forcing hypothesis removes the subtracted constant from the mean-zero test normalization.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.upperFace_reflectedWeakEquationOnUnion_of_compactSupport_of_memLp_normalizedCubeMeasure
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeUpperFaceNeighbor Q i), upperFaceReflectedForcingIntegrand Q i F φ x
Compact-test upper-face reflected weak equation, with the right-hand side
given in the normalized cube L² measure used by the Poisson endpoint
interfaces.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.lowerFace_reflectedWeakEquationOnUnion_of_compactSupport_of_memLp_normalizedCubeMeasure
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
(i : Fin d)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedGradientPairingIntegrand Q i (fun (y : Vec d) => W.w.toH1Function.grad y) φ x = ∫ (x : Vec d) in openCubeSet Q ∪ openCubeSet (cubeLowerFaceNeighbor Q i), lowerFaceReflectedForcingIntegrand Q i F φ x
Compact-test lower-face reflected weak equation, with the right-hand side
given in the normalized cube L² measure used by the Poisson endpoint
interfaces.
theorem
HCPolySupport.MeanZeroNeumannPoissonSolution.weakEquationOnCube_of_compactSupport_of_memLp_normalizedCubeMeasure
{d : ℕ}
{Q : TriadicCube d}
{F : Vec d → ℝ}
(W : MeanZeroNeumannPoissonSolution Q F)
{φ : Vec d → ℝ}
(hφ : ContDiff ℝ (↑⊤) φ)
(hφs : HasCompactSupport φ)
(hmean : cubeAverage Q F = 0)
(hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q))
:
∫ (x : Vec d) in openCubeSet Q, vecDot (W.w.toH1Function.grad x) (euclideanGradient φ x) = ∫ (x : Vec d) in openCubeSet Q, F x * φ x
Compact-test weak equation on the original cube, with the right-hand side
given in the normalized cube L² measure used by the Poisson endpoint
interfaces.