Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedGlobalEnergy

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

Global energy of the reflected zero extensions

The global stopping argument applies to the zero extensions of the gradient and of the datum on the reflected parent cube. This file keeps the exact 3^d reflection factor and the sigma0⁻¹ datum normalization visible in the real cutoff used at the large scale.

noncomputable def HCPolySupport.CubeCalderonZygmund.reflectedStoppingRadius {d : ℕ} (m : ℤ) (depth : ℕ) : ℝ

The smallest scale used by the global good-lambda stopping argument.

Equations

• HCPolySupport.CubeCalderonZygmund.reflectedStoppingRadius m depth = HCPolySupport.cubeRadius (HCPolySupport.originCube d m) / (10 * 3 ^ depth)

noncomputable def HCPolySupport.CubeCalderonZygmund.reflectedGlobalSquaredEnergy {d : ℕ} (m : ℤ) (eps sigma0 : ℝ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (HP : Vec d → Vec d) : ℝ

The global squared energy of the two zero-extended reflected fields.

Equations

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

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

The source-cube expression exactly represented by the global reflected energy. The scalar normalization of the datum is deliberately explicit.

Equations

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

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

The real large-scale cutoff for the reflected fields. In particular, it contains both the exact outer reflection mass (3 : ℝ)^d and the squared scaled-datum factor (eps⁻¹)^2 * (sigma0⁻¹)^2.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.reflectedStoppingRadius_pos {d : ℕ} (m : ℤ) (depth : ℕ) : 0 < reflectedStoppingRadius m depth

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

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_reflectedParentGradientExtension {d : ℕ} (m : ℤ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) : ∫ (x : Vec d), ‖reflectedParentGradientExtension m uP x‖ ^ 2 = ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), ‖hilbertifyVecField uP.grad x‖ ^ 2

Zero-extending a parent gradient has exactly its parent-cube squared energy.

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_hilbertify_reflectedParentDatumExtension {d : ℕ} (m : ℤ) (HP : Vec d → Vec d) : ∫ (x : Vec d), ‖hilbertifyVecField (reflectedParentDatumExtension m HP) x‖ ^ 2 = ∫ (x : Vec d) in openCubeSet (originCube d (m + 1)), ‖hilbertifyVecField HP x‖ ^ 2

Zero-extending a parent vector datum has exactly its parent-cube squared energy in the Hilbert realization.

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

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_hilbertify_reflectedParentDatumExtension_eq_three_pow {d : ℕ} {m : ℤ} (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeDirichletOddReflectionVectorField (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

theorem HCPolySupport.CubeCalderonZygmund.memLp_reflectedParentGradientExtension_two {d : ℕ} (m : ℤ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) : MeasureTheory.MemLp (reflectedParentGradientExtension m uP) 2 MeasureTheory.volume

The zero extensions are globally square-integrable whenever their parent fields are square-integrable on the reflected parent cube.

theorem HCPolySupport.CubeCalderonZygmund.memLp_hilbertify_reflectedParentDatumExtension_two {d : ℕ} (m : ℤ) (HP : Vec d → Vec d) (hHP : MemVectorL2 (openCubeSet (originCube d (m + 1))) HP) : MeasureTheory.MemLp (hilbertifyVecField (reflectedParentDatumExtension m HP)) 2 MeasureTheory.volume

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

The reflected source datum supplies the global L² input needed by the good-lambda stopping construction after extension by zero.

theorem HCPolySupport.CubeCalderonZygmund.integrable_sqNorm_reflectedParentGradientExtension {d : ℕ} (m : ℤ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) : MeasureTheory.Integrable (fun (x : Vec d) => ‖reflectedParentGradientExtension m uP x‖ ^ 2) MeasureTheory.volume

The squared gradient of the zero extension is globally integrable.

theorem HCPolySupport.CubeCalderonZygmund.integrable_sqNorm_smul_hilbertify_reflectedParentDatumExtension {d : ℕ} (m : ℤ) (sigma0 : ℝ) (HP : Vec d → Vec d) (hHP : MemVectorL2 (openCubeSet (originCube d (m + 1))) HP) : MeasureTheory.Integrable (fun (x : Vec d) => ‖sigma0⁻¹ • hilbertifyVecField (reflectedParentDatumExtension m HP) x‖ ^ 2) MeasureTheory.volume

The squared scaled datum of the zero extension is globally integrable.

theorem HCPolySupport.CubeCalderonZygmund.integrable_sqNorm_smul_hilbertify_reflectedParentDatumExtension_of_reflection {d : ℕ} {m : ℤ} (sigma0 : ℝ) (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeDirichletOddReflectionVectorField (originCube d m) H) : MeasureTheory.Integrable (fun (x : Vec d) => ‖sigma0⁻¹ • hilbertifyVecField (reflectedParentDatumExtension m HP) x‖ ^ 2) MeasureTheory.volume

theorem HCPolySupport.CubeCalderonZygmund.integral_sqNorm_smul_hilbertify_reflectedParentDatumExtension_eq_three_pow {d : ℕ} {m : ℤ} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (H HP : Vec d → Vec d) (hH : MemVectorL2 (openCubeSet (originCube d m)) H) (hHP : HP = cubeDirichletOddReflectionVectorField (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

The exact scalar rescaling of the reflected datum energy.

theorem HCPolySupport.CubeCalderonZygmund.reflectedGlobalSquaredEnergy_eq_reflectedSourceSquaredEnergy {d : ℕ} {m : ℤ} {eps sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H10Function (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 = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) (hHP : HP = cubeDirichletOddReflectionVectorField (originCube d m) H) : reflectedGlobalSquaredEnergy m eps sigma0 uP HP = reflectedSourceSquaredEnergy m eps sigma0 u H

The global squared energy of the zero-extended reflected fields is exactly 3^d times the Euclidean source-cube energy, including the scaled datum factor.

theorem HCPolySupport.CubeCalderonZygmund.reflectedGoodLambdaCutoff_eq_globalEnergy {d : ℕ} {m : ℤ} {depth : ℕ} {eps sigma0 : ℝ} (hsigma0 : 0 < sigma0) (u : H10Function (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 = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) (hHP : HP = cubeDirichletOddReflectionVectorField (originCube d m) H) : reflectedGoodLambdaCutoff m depth eps sigma0 u H = √(((2 * reflectedStoppingRadius m depth) ^ d)⁻¹ * reflectedGlobalSquaredEnergy m eps sigma0 uP HP)

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

theorem HCPolySupport.CubeCalderonZygmund.reflectedGoodLambdaCutoff_pos_of_sourceSquaredEnergy_pos {d : ℕ} (m : ℤ) (depth : ℕ) (eps sigma0 : ℝ) (u : H10Function (openCubeSet (originCube d m))) (H : Vec d → Vec d) (henergy : 0 < reflectedSourceSquaredEnergy m eps sigma0 u H) : 0 < reflectedGoodLambdaCutoff m depth eps sigma0 u H

A nontrivial source energy makes the large-scale cutoff strictly positive. This is intentionally conditional: zero source data have zero cutoff.