CubeTranslationFiniteP

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

Finite-exponent translation on triadic cubes

This file packages the exact translation from an arbitrary triadic cube to the centered cube of the same scale. Both directions use normalizedCubeMeasure; in particular, no unnormalized-volume factor enters the transport.

noncomputable def HCPolySupport.CubeCalderonZygmund.pullbackToOrigin {d : ℕ} {E : Type u_1} (Q : TriadicCube d) (F : Vec d → E) : Vec d → E

Pull a field on Q back to the centered cube of the same scale.

Equations

• HCPolySupport.CubeCalderonZygmund.pullbackToOrigin Q F x = F (x + HCPolySupport.triadicCubeShift Q)

noncomputable def HCPolySupport.CubeCalderonZygmund.pushforwardFromOrigin {d : ℕ} {E : Type u_1} (Q : TriadicCube d) (F : Vec d → E) : Vec d → E

Push a field on the centered cube to Q.

Equations

• HCPolySupport.CubeCalderonZygmund.pushforwardFromOrigin Q F x = F (x - HCPolySupport.triadicCubeShift Q)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.pushforwardFromOrigin_pullbackToOrigin {d : ℕ} {E : Type u_1} (Q : TriadicCube d) (F : Vec d → E) : pushforwardFromOrigin Q (pullbackToOrigin Q F) = F

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.pullbackToOrigin_pushforwardFromOrigin {d : ℕ} {E : Type u_1} (Q : TriadicCube d) (F : Vec d → E) : pullbackToOrigin Q (pushforwardFromOrigin Q F) = F

theorem HCPolySupport.CubeCalderonZygmund.measurePreserving_subRight_normalizedCubeMeasure_originCube {d : ℕ} (Q : TriadicCube d) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x - triadicCubeShift Q) (normalizedCubeMeasure Q) (normalizedCubeMeasure (originCube d Q.scale))

Subtracting the cube shift preserves the normalized cube measure in the reverse direction.

theorem HCPolySupport.CubeCalderonZygmund.memLp_pullbackToOrigin {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) {p : ENNReal} {F : Vec d → E} (hF : MeasureTheory.MemLp F p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale))

MemLp is preserved when a field is pulled back to the centered cube.

theorem HCPolySupport.CubeCalderonZygmund.memLp_pushforwardFromOrigin {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) {p : ENNReal} {F : Vec d → E} (hF : MeasureTheory.MemLp F p (normalizedCubeMeasure (originCube d Q.scale))) : MeasureTheory.MemLp (pushforwardFromOrigin Q F) p (normalizedCubeMeasure Q)

MemLp is preserved when a centered field is pushed forward to Q.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_pullbackToOrigin_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) {F : Vec d → E} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale)) = MeasureTheory.eLpNorm F p (normalizedCubeMeasure Q)

Pullback preserves the extended normalized Lᵖ norm.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_pushforwardFromOrigin_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) {F : Vec d → E} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure (originCube d Q.scale))) : MeasureTheory.eLpNorm (pushforwardFromOrigin Q F) p (normalizedCubeMeasure Q) = MeasureTheory.eLpNorm F p (normalizedCubeMeasure (originCube d Q.scale))

Pushforward preserves the extended normalized Lᵖ norm.

theorem HCPolySupport.CubeCalderonZygmund.cubeLpNorm_pullbackToOrigin_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) {F : Vec d → E} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : cubeLpNorm (originCube d Q.scale) p (pullbackToOrigin Q F) = cubeLpNorm Q p F

Pullback preserves the real normalized cube Lᵖ norm.

theorem HCPolySupport.CubeCalderonZygmund.cubeLpNorm_pushforwardFromOrigin_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) {F : Vec d → E} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure (originCube d Q.scale))) : cubeLpNorm Q p (pushforwardFromOrigin Q F) = cubeLpNorm (originCube d Q.scale) p F

Pushforward preserves the real normalized cube Lᵖ norm.

theorem HCPolySupport.CubeCalderonZygmund.memLp_vec_pullbackToOrigin {d : ℕ} (Q : TriadicCube d) {p : ENNReal} {F : Vec d → Vec d} (hF : MeasureTheory.MemLp F p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale))

Raw vector fields retain MemLp under pullback.

theorem HCPolySupport.CubeCalderonZygmund.memLp_hilbertVec_pullbackToOrigin {d : ℕ} (Q : TriadicCube d) {p : ENNReal} {F : Vec d → HilbertVec d} (hF : MeasureTheory.MemLp F p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale))

Hilbert-realized vector fields retain MemLp under pullback.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_vec_pullbackToOrigin_eq {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {F : Vec d → Vec d} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale)) = MeasureTheory.eLpNorm F p (normalizedCubeMeasure Q)

Raw vector fields retain their extended normalized norm under pullback.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_hilbertVec_pullbackToOrigin_eq {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {F : Vec d → HilbertVec d} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm (pullbackToOrigin Q F) p (normalizedCubeMeasure (originCube d Q.scale)) = MeasureTheory.eLpNorm F p (normalizedCubeMeasure Q)

Hilbert-realized vector fields retain their extended normalized norm under pullback.

theorem HCPolySupport.CubeCalderonZygmund.cubeLpNorm_vec_pullbackToOrigin_eq {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {F : Vec d → Vec d} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : cubeLpNorm (originCube d Q.scale) p (pullbackToOrigin Q F) = cubeLpNorm Q p F

Raw vector fields retain their real normalized cube norm under pullback.

theorem HCPolySupport.CubeCalderonZygmund.cubeLpNorm_hilbertVec_pullbackToOrigin_eq {d : ℕ} (Q : TriadicCube d) (p : ENNReal) {F : Vec d → HilbertVec d} (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : cubeLpNorm (originCube d Q.scale) p (pullbackToOrigin Q F) = cubeLpNorm Q p F

Hilbert-realized vector fields retain their real normalized cube norm under pullback.

noncomputable def HCPolySupport.CubeCalderonZygmund.untranslateH10ToOrigin {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) : H10Function (openCubeSet (originCube d Q.scale))

Pull an arbitrary-cube zero-trace function back to the centered cube.

Equations

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

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.untranslateH10ToOrigin_toFun {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (x : Vec d) : (untranslateH10ToOrigin Q u).toFun x = u.toFun (x + triadicCubeShift Q)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.untranslateH10ToOrigin_grad {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) (x : Vec d) : (untranslateH10ToOrigin Q u).grad x = u.grad (x + triadicCubeShift Q)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.pushforwardFromOrigin_untranslateH10ToOrigin_grad {d : ℕ} (Q : TriadicCube d) (u : H10Function (openCubeSet Q)) : pushforwardFromOrigin Q (untranslateH10ToOrigin Q u).grad = u.grad

Pushing the centered pullback gradient forward recovers the original arbitrary-cube gradient exactly.

noncomputable def HCPolySupport.CubeCalderonZygmund.untranslateH1MeanZeroToOrigin {d : ℕ} (Q : TriadicCube d) (u : H1MeanZeroFunction (openCubeSet Q)) : H1MeanZeroFunction (openCubeSet (originCube d Q.scale))

Pull an arbitrary-cube mean-zero function back to the centered cube.

Equations

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

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.untranslateH1MeanZeroToOrigin_toFun {d : ℕ} (Q : TriadicCube d) (u : H1MeanZeroFunction (openCubeSet Q)) (x : Vec d) : (untranslateH1MeanZeroToOrigin Q u).toH1Function.toFun x = u.toH1Function.toFun (x + triadicCubeShift Q)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.untranslateH1MeanZeroToOrigin_grad {d : ℕ} (Q : TriadicCube d) (u : H1MeanZeroFunction (openCubeSet Q)) (x : Vec d) : (untranslateH1MeanZeroToOrigin Q u).toH1Function.grad x = u.toH1Function.grad (x + triadicCubeShift Q)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.pushforwardFromOrigin_untranslateH1MeanZeroToOrigin_grad {d : ℕ} (Q : TriadicCube d) (u : H1MeanZeroFunction (openCubeSet Q)) : pushforwardFromOrigin Q (untranslateH1MeanZeroToOrigin Q u).toH1Function.grad = u.toH1Function.grad

Pushing the centered mean-zero pullback gradient forward recovers the original arbitrary-cube gradient exactly.

theorem HCPolySupport.CubeCalderonZygmund.isZeroTraceDirichletRhsWeakSolution_untranslateH10ToOrigin {d : ℕ} (Q : TriadicCube d) (A : Mat d) {u : H10Function (openCubeSet Q)} {F : Vec d → Vec d} (hu : IsZeroTraceDirichletRhsWeakSolution (fun (x : Vec d) => A) (openCubeSet Q) u fun (x : Vec d) => -F x) : IsZeroTraceDirichletRhsWeakSolution (fun (x : Vec d) => A) (openCubeSet (originCube d Q.scale)) (untranslateH10ToOrigin Q u) fun (x : Vec d) => -pullbackToOrigin Q F x

Pull the constant-coefficient Dirichlet divergence equation with datum -F from an arbitrary cube to the centered cube of the same scale.

theorem HCPolySupport.CubeCalderonZygmund.isMeanZeroNeumannRhsWeakSolution_untranslateH1MeanZeroToOrigin {d : ℕ} (Q : TriadicCube d) (A : Mat d) {u : H1MeanZeroFunction (openCubeSet Q)} {F : Vec d → Vec d} (hu : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => A) (openCubeSet Q) u fun (x : Vec d) => -F x) : IsMeanZeroNeumannRhsWeakSolution (fun (x : Vec d) => A) (openCubeSet (originCube d Q.scale)) (untranslateH1MeanZeroToOrigin Q u) fun (x : Vec d) => -pullbackToOrigin Q F x

Pull the constant-coefficient Neumann divergence equation with datum -F from an arbitrary cube to the centered cube of the same scale.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_hilbertify_le_dimension_mul_vec {d : ℕ} {p : ENNReal} {Q : TriadicCube d} (F : Vec d → Vec d) (hF : MeasureTheory.AEStronglyMeasurable F (normalizedCubeMeasure Q)) : MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (F x)) p (normalizedCubeMeasure Q) ≤ ENNReal.ofReal ↑d * MeasureTheory.eLpNorm F p (normalizedCubeMeasure Q)

The Hilbert realization has Lp norm bounded by dimension times the coordinate norm.