ReflectedGlobalEnergy

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

Global energy for centered-Neumann even reflection

The centered-Neumann good-lambda argument uses the same parent-cube zero extensions as the Dirichlet argument, but the solution gradient and datum are transported by the coordinate-fold even reflection. This file identifies the actual global energy of those extensions with its source-cube expression.

noncomputable def HCPolySupport.CubeCalderonZygmund.neumannReflectedSourceSquaredEnergy {d : ℕ} (m : ℤ) (eps sigma0 : ℝ) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (H : Vec d → Vec d) : ℝ

Source-cube squared energy represented by the zero-extended Neumann even reflections on the centered parent.

Equations

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

noncomputable def HCPolySupport.CubeCalderonZygmund.neumannReflectedGoodLambdaCutoff {d : ℕ} (m : ℤ) (depth : ℕ) (eps sigma0 : ℝ) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (H : Vec d → Vec d) : ℝ

Natural large-scale cutoff formed from the exact reflected Neumann source energy.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.neumannReflectedGoodLambdaCutoff_nonneg {d : ℕ} (m : ℤ) (depth : ℕ) (eps sigma0 : ℝ) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (H : Vec d → Vec d) : 0 ≤ neumannReflectedGoodLambdaCutoff m depth eps sigma0 u H

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_reflectedParentGradientExtension_eq_three_pow_of_evenReflection {d : ℕ} {m : ℤ} (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (huP : uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.toH1Function.grad y) : ∫ (x : Vec d), ‖reflectedParentGradientExtension m uP x‖ ^ 2 = 3 ^ d * ∫ (x : Vec d) in openCubeSet (originCube d m), ‖hilbertifyVecField u.toH1Function.grad x‖ ^ 2

The zero-extended gradient of an even-reflected centered-Neumann solution has exactly 3^d times its source-cube squared energy.

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_hilbertify_reflectedParentDatumExtension_eq_three_pow_of_evenReflection {d : ℕ} {m : ℤ} (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeCoordinateFoldReflectedVectorField (originCube d m) H) : ∫ (x : Vec d), ‖hilbertifyVecField (reflectedParentDatumExtension m HP) x‖ ^ 2 = 3 ^ d * ∫ (x : Vec d) in openCubeSet (originCube d m), ‖hilbertifyVecField H x‖ ^ 2

The zero-extended even-reflected datum has exactly 3^d times its source-cube squared energy.

theorem HCPolySupport.CubeCalderonZygmund.memLp_hilbertify_reflectedParentDatumExtension_two_of_evenReflection {d : ℕ} {m : ℤ} (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeCoordinateFoldReflectedVectorField (originCube d m) H) : MeasureTheory.MemLp (hilbertifyVecField (reflectedParentDatumExtension m HP)) 2 MeasureTheory.volume

The even-reflected source datum is globally square-integrable after parent restriction and extension by zero.

theorem HCPolySupport.CubeCalderonZygmund.integral_reflectedParentDatum_normSq_eq_scaledSource {d : ℕ} {m : ℤ} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeCoordinateFoldReflectedVectorField (originCube d m) H) : ∫ (x : Vec d), ‖sigma0⁻¹ • hilbertifyVecField (reflectedParentDatumExtension m HP) x‖ ^ 2 = sigma0⁻¹ ^ 2 * 3 ^ d * ∫ (x : Vec d) in openCubeSet (originCube d m), ‖hilbertifyVecField H x‖ ^ 2

Exact scalar rescaling of the even-reflected datum energy.

theorem HCPolySupport.CubeCalderonZygmund.reflectedGlobalSquaredEnergy_eq_neumannReflectedSourceSquaredEnergy {d : ℕ} {m : ℤ} {eps sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (huP : uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.toH1Function.grad y) (hHP : HP = cubeCoordinateFoldReflectedVectorField (originCube d m) H) : reflectedGlobalSquaredEnergy m eps sigma0 uP HP = neumannReflectedSourceSquaredEnergy m eps sigma0 u H

The global squared energy of the actual zero extensions agrees exactly with the centered-Neumann source energy.

theorem HCPolySupport.CubeCalderonZygmund.neumannReflectedGoodLambdaCutoff_eq_globalEnergy {d : ℕ} {m : ℤ} {depth : ℕ} {eps sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H1MeanZeroFunction (openCubeSet (originCube d m))) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (huP : uP.grad = cubeCoordinateFoldReflectedVectorField (originCube d m) fun (y : Vec d) => u.toH1Function.grad y) (hHP : HP = cubeCoordinateFoldReflectedVectorField (originCube d m) H) : neumannReflectedGoodLambdaCutoff m depth eps sigma0 u H = √(((2 * reflectedStoppingRadius m depth) ^ d)⁻¹ * reflectedGlobalSquaredEnergy m eps sigma0 uP HP)

The source-facing Neumann cutoff is exactly the cutoff formed from the global energy of the actual zero extensions.