Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.ReflectionParentApprox

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

theorem HCPolySupport.toReal_eLpNorm_two_sq_eq_integral_norm_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : (MeasureTheory.eLpNorm f 2 μ).toReal ^ 2 = ∫ (x : α), ‖f x‖ ^ 2 ∂μ

For Hilbert-valued L² functions, the square of the toReal eLpNorm is the integral of the pointwise squared norm.

@[simp]

theorem HCPolySupport.cubeCoordinateFoldReflectedScalar_sub_apply {d : ℕ} (Q : TriadicCube d) (F U : Vec d → ℝ) (x : Vec d) : cubeCoordinateFoldReflectedScalar Q (fun (y : Vec d) => F y - U y) x = cubeCoordinateFoldReflectedScalar Q F x - cubeCoordinateFoldReflectedScalar Q U x

Scalar all-face reflection distributes over subtraction.

@[simp]

theorem HCPolySupport.cubeCoordinateFoldReflectedVectorField_sub_apply {d : ℕ} (Q : TriadicCube d) (G H : Vec d → Vec d) (x : Vec d) : cubeCoordinateFoldReflectedVectorField Q (fun (y : Vec d) => G y - H y) x = cubeCoordinateFoldReflectedVectorField Q G x - cubeCoordinateFoldReflectedVectorField Q H x

Vector all-face reflection distributes over subtraction.

theorem HCPolySupport.memScalarL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedScalar_sub {d : ℕ} {m : ℤ} {F U : Vec d → ℝ} (hFU : MemScalarL2 (openCubeSet (originCube d m)) fun (x : Vec d) => F x - U x) : MemScalarL2 (openCubeSet (originCube d (m + 1))) fun (x : Vec d) => cubeCoordinateFoldReflectedScalar (originCube d m) F x - cubeCoordinateFoldReflectedScalar (originCube d m) U x

Reflected scalar differences are L² on the centered parent cube whenever the original difference is L² on the origin cube.

theorem HCPolySupport.memVectorL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField_sub {d : ℕ} {m : ℤ} {G H : Vec d → Vec d} (hGH : MemVectorL2 (openCubeSet (originCube d m)) fun (x : Vec d) => G x - H x) : MemVectorL2 (openCubeSet (originCube d (m + 1))) fun (x : Vec d) => cubeCoordinateFoldReflectedVectorField (originCube d m) G x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x

Reflected vector-field differences are L² on the centered parent cube whenever the original difference is L² on the origin cube.

theorem HCPolySupport.setIntegral_successorCube_foldedReflectedScalar_sub_sq {d : ℕ} {m : ℤ} {F U : Vec d → ℝ} (hFU : MemScalarL2 (openCubeSet (originCube d m)) fun (x : Vec d) => F x - U x) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), (cubeCoordinateFoldReflectedScalar (originCube d m) F x - cubeCoordinateFoldReflectedScalar (originCube d m) U x) * (cubeCoordinateFoldReflectedScalar (originCube d m) F x - cubeCoordinateFoldReflectedScalar (originCube d m) U x) = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), (F y - U y) * (F y - U y)

Scalar reflected-difference energy on the centered parent cube is 3^d copies of the original difference energy.

theorem HCPolySupport.setIntegral_successorCube_foldedReflectedVectorField_sub_self_pairing {d : ℕ} {m : ℤ} {G H : Vec d → Vec d} (hGH : MemVectorL2 (openCubeSet (originCube d m)) fun (x : Vec d) => G x - H x) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (cubeCoordinateFoldReflectedVectorField (originCube d m) G x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x) (cubeCoordinateFoldReflectedVectorField (originCube d m) G x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x) = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), vecDot (G y - H y) (G y - H y)

Vector reflected-difference energy on the centered parent cube is 3^d copies of the original difference energy.

theorem HCPolySupport.tendsto_eLpNorm_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedScalar_sub {d : ℕ} {m : ℤ} {F : ℕ → Vec d → ℝ} {U : Vec d → ℝ} (hFU : ∀ (n : ℕ), MemScalarL2 (openCubeSet (originCube d m)) fun (x : Vec d) => F n x - U x) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - U x) 2 (volumeMeasureOn (openCubeSet (originCube d m)))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => cubeCoordinateFoldReflectedScalar (originCube d m) (F n) x - cubeCoordinateFoldReflectedScalar (originCube d m) U x) 2 (volumeMeasureOn (openCubeSet (originCube d (m + 1))))) Filter.atTop (nhds 0)

Scalar L² convergence on the original cube transfers to the all-face reflected scalar differences on the centered parent cube.

theorem HCPolySupport.setIntegral_successorCube_foldedReflectedVectorField_sub_coord_sq {d : ℕ} {m : ℤ} {G H : Vec d → Vec d} (j : Fin d) (hGHj : MemScalarL2 (openCubeSet (originCube d m)) fun (x : Vec d) => G x j - H x j) : ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), (cubeCoordinateFoldReflectedVectorField (originCube d m) G x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x) j * (cubeCoordinateFoldReflectedVectorField (originCube d m) G x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x) j = 3 ^ d * ∫ (y : Vec d) in openCubeSet (originCube d m), (G y j - H y j) * (G y j - H y j)

A coordinate of a reflected vector-field difference has the same 3^d energy transfer as a reflected scalar difference.

theorem HCPolySupport.tendsto_eLpNorm_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField_sub_coord {d : ℕ} {m : ℤ} {G : ℕ → Vec d → Vec d} {H : Vec d → Vec d} (j : Fin d) (hGH : ∀ (n : ℕ), MemVectorL2 (openCubeSet (originCube d m)) fun (x : Vec d) => G n x - H x) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => G n x j - H x j) 2 (volumeMeasureOn (openCubeSet (originCube d m)))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (cubeCoordinateFoldReflectedVectorField (originCube d m) (G n) x - cubeCoordinateFoldReflectedVectorField (originCube d m) H x) j) 2 (volumeMeasureOn (openCubeSet (originCube d (m + 1))))) Filter.atTop (nhds 0)

Coordinatewise L² convergence on the original cube transfers to coordinates of the all-face reflected vector-field differences on the centered parent cube.

theorem HCPolySupport.tendsto_toScalarL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedScalar {d : ℕ} {m : ℤ} {F : ℕ → Vec d → ℝ} {U : Vec d → ℝ} (hF : ∀ (n : ℕ), MemScalarL2 (openCubeSet (originCube d m)) (F n)) (hU : MemScalarL2 (openCubeSet (originCube d m)) U) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => F n x - U x) 2 (volumeMeasureOn (openCubeSet (originCube d m)))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => toScalarL2 ⋯) Filter.atTop (nhds (toScalarL2 ⋯))

Scalar L² convergence transfer, stated directly in the ScalarL2 classes on the centered parent cube.

theorem HCPolySupport.tendsto_toScalarL2_openCubeSet_succ_originCube_cubeCoordinateFoldReflectedVectorField_coord {d : ℕ} {m : ℤ} {G : ℕ → Vec d → Vec d} {H : Vec d → Vec d} (j : Fin d) (hG : ∀ (n : ℕ), MemVectorL2 (openCubeSet (originCube d m)) (G n)) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hlim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => G n x j - H x j) 2 (volumeMeasureOn (openCubeSet (originCube d m)))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => toScalarL2 ⋯) Filter.atTop (nhds (toScalarL2 ⋯))

Coordinatewise reflected-gradient convergence transfer, stated directly in the ScalarL2 classes on the centered parent cube.