Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.SourceParentFiniteLpExtension

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

Source-supported finite-L^p data on a centered parent cube

This module packages extension by zero from an origin cube into its centered parent, retaining both the finite-exponent and energy memberships.

theorem HCPolySupport.CubeCalderonZygmund.normalizedCubeMeasure_parent_restrict_source {d : ℕ} (m : ℤ) : (normalizedCubeMeasure (originCube d (m + 1))).restrict (openCubeSet (originCube d m)) = (3 ^ d)⁻¹ • normalizedCubeMeasure (originCube d m)

noncomputable def HCPolySupport.CubeCalderonZygmund.sourceParentFiniteLpExtension {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : CubeEuclideanL2LpField (originCube d (m + 1)) q

The source datum, extended by zero, as finite-L^p data on the centered parent cube.

Equations

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

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.sourceParentFiniteLpExtension_toField {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : (sourceParentFiniteLpExtension m q h).toField = openParentDatumExtension (openCubeSet (originCube d m)) h.toField

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_sourceParentFiniteLpExtension {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : MeasureTheory.eLpNorm (hilbertifyVecField (sourceParentFiniteLpExtension m q h).toField) q.exponent (normalizedCubeMeasure (originCube d (m + 1))) = (3 ^ d)⁻¹ ^ q.exponent.toReal⁻¹ * MeasureTheory.eLpNorm (hilbertifyVecField h.toField) q.exponent (normalizedCubeMeasure (originCube d m))

The normalized finite-exponent norm of a datum extended by zero to its centered parent has the exact probability-mass factor.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_sourceParentFiniteLpExtension_le {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : MeasureTheory.eLpNorm (hilbertifyVecField (sourceParentFiniteLpExtension m q h).toField) q.exponent (normalizedCubeMeasure (originCube d (m + 1))) ≤ MeasureTheory.eLpNorm (hilbertifyVecField h.toField) q.exponent (normalizedCubeMeasure (originCube d m))

The source-supported parent extension cannot increase the normalized finite-exponent Euclidean norm.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_two_sourceParentFiniteLpExtension {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : MeasureTheory.eLpNorm (hilbertifyVecField (sourceParentFiniteLpExtension m q h).toField) 2 (normalizedCubeMeasure (originCube d (m + 1))) = (3 ^ d)⁻¹ ^ (1 / 2).toReal * MeasureTheory.eLpNorm (hilbertifyVecField h.toField) 2 (normalizedCubeMeasure (originCube d m))

The normalized L² norm of a source-supported parent extension has the same exact probability-mass factor.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_two_sourceParentFiniteLpExtension_le {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : MeasureTheory.eLpNorm (hilbertifyVecField (sourceParentFiniteLpExtension m q h).toField) 2 (normalizedCubeMeasure (originCube d (m + 1))) ≤ MeasureTheory.eLpNorm (hilbertifyVecField h.toField) 2 (normalizedCubeMeasure (originCube d m))

The source-supported parent extension cannot increase its normalized Euclidean L² norm.

theorem HCPolySupport.CubeCalderonZygmund.memVectorL2_sourceParentFiniteLpExtension {d : ℕ} (m : ℤ) (q : FiniteLpExponent) (h : CubeEuclideanL2LpField (originCube d m) q) : MemVectorL2 (openCubeSet (originCube d (m + 1))) (sourceParentFiniteLpExtension m q h).toField

The parent extension is a raw vector L² datum on the open parent cube, as needed by the canonical adjoint solver.