Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.AxisCubeHarmonicCovariance

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

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeCenter {d : ℕ} (z : Vec d) (L : ℝ) : Vec d

The center of the open axis cube axisCube z L.

Equations

• HCPolySupport.CubeCalderonZygmund.axisCubeCenter z L i = z i + L / 2

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeAffine {d : ℕ} (z : Vec d) (L : ℝ) : Vec d → Vec d

The affine formula which, for positive L, maps the centered unit triadic cube to axisCube z L.

Equations

• HCPolySupport.CubeCalderonZygmund.axisCubeAffine z L x = L • x + HCPolySupport.CubeCalderonZygmund.axisCubeCenter z L

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeAffineInv {d : ℕ} (z : Vec d) (L : ℝ) : Vec d → Vec d

The inverse affine formula, which is an actual inverse when L ≠ 0.

Equations

• HCPolySupport.CubeCalderonZygmund.axisCubeAffineInv z L x = L⁻¹ • (x - HCPolySupport.CubeCalderonZygmund.axisCubeCenter z L)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffineInv_axisCubeAffine {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (x : Vec d) : axisCubeAffineInv z L (axisCubeAffine z L x) = x

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_axisCubeAffineInv {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (x : Vec d) : axisCubeAffine z L (axisCubeAffineInv z L x) = x

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeAffineMeasurableEquiv {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) : Vec d ≃ᵐ Vec d

The affine parametrization as a measurable equivalence of the ambient Euclidean space when its scale is nonzero.

Equations

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

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffineMeasurableEquiv_apply {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (x : Vec d) : (axisCubeAffineMeasurableEquiv z hL) x = axisCubeAffine z L x

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffineMeasurableEquiv_symm_apply {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (x : Vec d) : (axisCubeAffineMeasurableEquiv z hL).symm x = axisCubeAffineInv z L x

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_comp {d : ℕ} (z w : Vec d) (L S : ℝ) (x : Vec d) : axisCubeAffine z L (axisCubeAffine w S x) = axisCubeAffine (fun (i : Fin d) => L * w i + axisCubeCenter z L i) (L * S) x

theorem HCPolySupport.CubeCalderonZygmund.openCubeSet_originCube_zero_eq_centered_axisCube {d : ℕ} : openCubeSet (originCube d 0) = axisCube (fun (x : Fin d) => -(1 / 2)) 1

theorem HCPolySupport.CubeCalderonZygmund.axisCube_eq_translateSet_smul_openCubeSet_originCube_zero {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) : axisCube z L = translateSet (axisCubeCenter z L) (L • openCubeSet (originCube d 0))

An arbitrary positive-length axis cube is the centered-unit triadic cube, dilated by its side length and translated to its center.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_image_openCubeSet_originCube_zero {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) : axisCubeAffine z L '' openCubeSet (originCube d 0) = axisCube z L

The positive affine parametrization maps the centered unit cube exactly onto its target axis cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_preimage_axisCube {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) : axisCubeAffine z L ⁻¹' axisCube z L = openCubeSet (originCube d 0)

The target axis cube has the centered unit cube as its exact preimage under the positive affine parametrization.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_image_axisCube {d : ℕ} (z w : Vec d) (L S : ℝ) (hL : 0 < L) (hS : 0 < S) : axisCubeAffine z L '' axisCube w S = axisCube (fun (i : Fin d) => L * w i + axisCubeCenter z L i) (L * S)

A positive affine cube parametrization maps every positive axis cube to the axis cube with the expected affine corner and product side length.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_preimage_axisCube_affine {d : ℕ} (z w : Vec d) (L S : ℝ) (hL : 0 < L) (hS : 0 < S) : axisCubeAffine z L ⁻¹' axisCube (fun (i : Fin d) => L * w i + axisCubeCenter z L i) (L * S) = axisCube w S

Exact preimage form of axisCubeAffine_image_axisCube.

noncomputable def HCPolySupport.CubeCalderonZygmund.triadicCubeAxisCorner {d : ℕ} (Q : TriadicCube d) : Vec d

Lower corner of the open axis-cube realization of a triadic cube.

Equations

• HCPolySupport.CubeCalderonZygmund.triadicCubeAxisCorner Q i = (↑(Q.index i) - 1 / 2) * HCPolySupport.cubeScaleFactor Q

theorem HCPolySupport.CubeCalderonZygmund.openCubeSet_eq_axisCube_triadicCube {d : ℕ} (Q : TriadicCube d) : openCubeSet Q = axisCube (triadicCubeAxisCorner Q) (cubeScaleFactor Q)

Every open triadic cube is exactly its lower-corner axis cube.

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthSide (L : ℝ) (n : ℕ) : ℝ

Side length of the concentric depth-n contraction of axisCube z L.

Equations

• HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthSide L n = L * 3 ^ (-↑n)

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthSide_zero (L : ℝ) : axisCubeConcentricDepthSide L 0 = L

theorem HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthSide_pos {L : ℝ} (hL : 0 < L) (n : ℕ) : 0 < axisCubeConcentricDepthSide L n

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthCorner {d : ℕ} (z : Vec d) (L : ℝ) (n : ℕ) : Vec d

Lower corner of the concentric depth-n contraction of axisCube z L.

Equations

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

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeConcentricDepthCorner_zero {d : ℕ} (z : Vec d) (L : ℝ) : axisCubeConcentricDepthCorner z L 0 = z

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_image_openCubeSet_originCube_neg_nat {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) (n : ℕ) : axisCubeAffine z L '' openCubeSet (originCube d (-↑n)) = axisCube (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n)

The outer affine parametrization maps the centered depth-n source cube exactly to the corresponding concentric contraction of its target cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeAffine_preimage_concentricDepthAxisCube {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) (n : ℕ) : axisCubeAffine z L ⁻¹' axisCube (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n) = openCubeSet (originCube d (-↑n))

Exact preimage form of the fixed concentric depth transport.

theorem HCPolySupport.CubeCalderonZygmund.WeakPoissonEquationOn.undilateSet_zero {d : ℕ} {U V : Set (Vec d)} {a : ℝ} (ha : 0 < a) (hV : V = a • U) {u : H1Function V} (h : WeakPoissonEquationOn V u 0) : WeakPoissonEquationOn U (H1Function.undilateSet ha hV u) 0

Homogeneous weak Poisson equations are invariant under the gradient-preserving pullback from a • U to U.

theorem HCPolySupport.CubeCalderonZygmund.WeakPoissonEquationOn.untranslate_zero {d : ℕ} {U : Set (Vec d)} {z : Vec d} {u : H1Function (translateSet z U)} (h : WeakPoissonEquationOn (translateSet z U) u 0) : WeakPoissonEquationOn U (H1Function.untranslate z u) 0

Homogeneous weak Poisson equations are invariant under translation pullback.

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeHarmonicPullback {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) : H1Function (openCubeSet (originCube d 0))

Pull an H¹ function on a positive-length axis cube back to the fixed centered unit triadic cube, with the standard value normalization that leaves the gradient unscaled.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.axisCubeHarmonicPullback_weakPoisson_zero {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) {u : H1Function (axisCube z L)} (h : WeakPoissonEquationOn (axisCube z L) u 0) : WeakPoissonEquationOn (openCubeSet (originCube d 0)) (axisCubeHarmonicPullback z hL u) 0

Pullback to the centered unit cube preserves the homogeneous weak Poisson equation.

noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeNormalizedMeasure {d : ℕ} (z : Vec d) (L : ℝ) : MeasureTheory.Measure (Vec d)

The pushforward of centered-unit Lebesgue measure through the affine map. For positive L, axisCubeNormalizedMeasure_eq_smul_volume_restrict below identifies this with normalized Lebesgue measure on axisCube z L. No such axis-cube interpretation is claimed for nonpositive L.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalizedMeasure_eq_smul_volume_restrict {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) : axisCubeNormalizedMeasure z L = ENNReal.ofReal (L ^ d)⁻¹ • MeasureTheory.volume.restrict (axisCube z L)

For positive side length, the affine pushforward is exactly normalized Lebesgue measure on the target axis cube.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalizedMeasure_concentricDepth_eq_smul_volume_restrict {d : ℕ} (z : Vec d) (L : ℝ) (hL : 0 < L) (n : ℕ) : axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n) = ENNReal.ofReal (axisCubeConcentricDepthSide L n ^ d)⁻¹ • MeasureTheory.volume.restrict (axisCube (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Canonical normalized-volume form of the target measure at a fixed concentric depth.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalizedMeasure_triadicCube {d : ℕ} (Q : TriadicCube d) : axisCubeNormalizedMeasure (triadicCubeAxisCorner Q) (cubeScaleFactor Q) = normalizedCubeMeasure Q

On a triadic cube, the affine pushforward normalization agrees exactly with the project's canonical normalizedCubeMeasure.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_concentricDepth_eq_openCubeSet_centralDescendant {d : ℕ} (Q : TriadicCube d) (n : ℕ) : axisCube (axisCubeConcentricDepthCorner (triadicCubeAxisCorner Q) (cubeScaleFactor Q) n) (axisCubeConcentricDepthSide (cubeScaleFactor Q) n) = openCubeSet (centralDescendant Q n)

The concentric depth-n axis cube of a triadic cube is exactly its ordinary central depth-n descendant.

theorem HCPolySupport.CubeCalderonZygmund.axisCubeNormalizedMeasure_concentricDepth_eq_normalizedCubeMeasure_centralDescendant {d : ℕ} (Q : TriadicCube d) (n : ℕ) : axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner (triadicCubeAxisCorner Q) (cubeScaleFactor Q) n) (axisCubeConcentricDepthSide (cubeScaleFactor Q) n) = normalizedCubeMeasure (centralDescendant Q n)

The affine normalized measure on a concentric depth-n axis cube is the canonical normalized measure on the corresponding central descendant.

theorem HCPolySupport.CubeCalderonZygmund.map_axisCubeAffine_axisCubeNormalizedMeasure {d : ℕ} (z w : Vec d) (L S : ℝ) : MeasureTheory.Measure.map (axisCubeAffine z L) (axisCubeNormalizedMeasure w S) = axisCubeNormalizedMeasure (fun (i : Fin d) => L * w i + axisCubeCenter z L i) (L * S)

Affine pushforward of an affine-cube normalized measure is the normalized measure with the composed affine corner and product scale. This identity is purely a pushforward identity and therefore does not require positive scales.

theorem HCPolySupport.CubeCalderonZygmund.measurePreserving_axisCubeAffine {d : ℕ} (z : Vec d) (L : ℝ) : MeasureTheory.MeasurePreserving (axisCubeAffine z L) (MeasureTheory.volume.restrict (openCubeSet (originCube d 0))) (axisCubeNormalizedMeasure z L)

The affine map preserves the centered-unit source measure and its pushforward measure.

theorem HCPolySupport.CubeCalderonZygmund.measurePreserving_axisCubeAffineInv {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) : MeasureTheory.MeasurePreserving (axisCubeAffineInv z L) (axisCubeNormalizedMeasure z L) (MeasureTheory.volume.restrict (openCubeSet (originCube d 0)))

For nonzero scale, the inverse affine map preserves the pushforward measure back to centered-unit Lebesgue measure.

theorem HCPolySupport.CubeCalderonZygmund.aestronglyMeasurable_axisCubeAffine_iff {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) {E : Type u_1} [TopologicalSpace E] (f : Vec d → E) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => f (axisCubeAffine z L x)) (MeasureTheory.volume.restrict (openCubeSet (originCube d 0))) ↔ MeasureTheory.AEStronglyMeasurable f (axisCubeNormalizedMeasure z L)

Strong a.e. measurability can be transported in either direction through the nondegenerate affine parametrization.

theorem HCPolySupport.CubeCalderonZygmund.memLp_axisCubeAffine_iff {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) : MeasureTheory.MemLp (fun (x : Vec d) => f (axisCubeAffine z L x)) p (MeasureTheory.volume.restrict (openCubeSet (originCube d 0))) ↔ MeasureTheory.MemLp f p (axisCubeNormalizedMeasure z L)

MemLp is equivalent on the source and target of every nondegenerate affine cube parametrization. In particular, target integrability can be deduced from source integrability without a circular target-measurability hypothesis.

theorem HCPolySupport.CubeCalderonZygmund.map_axisCubeAffine_normalizedCubeMeasure_originCube_neg_nat {d : ℕ} (z : Vec d) (L : ℝ) (n : ℕ) : MeasureTheory.Measure.map (axisCubeAffine z L) (normalizedCubeMeasure (originCube d (-↑n))) = axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n)

The fixed centered depth-n source measure pushes forward to the exact normalized measure on the target concentric contraction.

theorem HCPolySupport.CubeCalderonZygmund.measurePreserving_axisCubeAffine_originCube_neg_nat {d : ℕ} (z : Vec d) (L : ℝ) (n : ℕ) : MeasureTheory.MeasurePreserving (axisCubeAffine z L) (normalizedCubeMeasure (originCube d (-↑n))) (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Measure-preserving form of the fixed concentric depth transport.

theorem HCPolySupport.CubeCalderonZygmund.measurePreserving_axisCubeAffineInv_originCube_neg_nat {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (n : ℕ) : MeasureTheory.MeasurePreserving (axisCubeAffineInv z L) (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n)) (normalizedCubeMeasure (originCube d (-↑n)))

Inverse measure-preserving form of the fixed concentric depth transport.

theorem HCPolySupport.CubeCalderonZygmund.aestronglyMeasurable_axisCubeAffine_originCube_neg_nat_iff {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (n : ℕ) {E : Type u_1} [TopologicalSpace E] (f : Vec d → E) : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => f (axisCubeAffine z L x)) (normalizedCubeMeasure (originCube d (-↑n))) ↔ MeasureTheory.AEStronglyMeasurable f (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Bidirectional strong a.e. measurability transport on a fixed concentric depth.

theorem HCPolySupport.CubeCalderonZygmund.memLp_axisCubeAffine_originCube_neg_nat_iff {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (n : ℕ) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) : MeasureTheory.MemLp (fun (x : Vec d) => f (axisCubeAffine z L x)) p (normalizedCubeMeasure (originCube d (-↑n))) ↔ MeasureTheory.MemLp f p (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Bidirectional MemLp transport on the fixed centered depth-n source and its target concentric contraction.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_axisCubeAffine {d : ℕ} (z : Vec d) (L : ℝ) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (axisCubeNormalizedMeasure z L)) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (axisCubeAffine z L x)) p (MeasureTheory.volume.restrict (openCubeSet (originCube d 0))) = MeasureTheory.eLpNorm f p (axisCubeNormalizedMeasure z L)

The affine parametrization preserves every extended Lᵖ norm when the target axis cube carries axisCubeNormalizedMeasure.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_axisCubeAffine_of_comp_aestronglyMeasurable {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => f (axisCubeAffine z L x)) (MeasureTheory.volume.restrict (openCubeSet (originCube d 0)))) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (axisCubeAffine z L x)) p (MeasureTheory.volume.restrict (openCubeSet (originCube d 0))) = MeasureTheory.eLpNorm f p (axisCubeNormalizedMeasure z L)

Source-side measurability is also sufficient for exact affine norm transport when the affine map is nondegenerate.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_axisCubeAffine_originCube_neg_nat {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (n : ℕ) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => f (axisCubeAffine z L x)) (normalizedCubeMeasure (originCube d (-↑n)))) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (axisCubeAffine z L x)) p (normalizedCubeMeasure (originCube d (-↑n))) = MeasureTheory.eLpNorm f p (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Exact extended Lᵖ norm transport from the fixed centered depth-n source cube to the corresponding target concentric contraction.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_axisCubeAffine_originCube_neg_nat_of_memLp {d : ℕ} (z : Vec d) {L : ℝ} (hL : L ≠ 0) (n : ℕ) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.MemLp (fun (x : Vec d) => f (axisCubeAffine z L x)) p (normalizedCubeMeasure (originCube d (-↑n)))) : MeasureTheory.eLpNorm (fun (x : Vec d) => f (axisCubeAffine z L x)) p (normalizedCubeMeasure (originCube d (-↑n))) = MeasureTheory.eLpNorm f p (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

MemLp on the fixed centered source supplies the measurability needed for the exact depth-n norm identity.

theorem HCPolySupport.CubeCalderonZygmund.eLpNormToReal_axisCubeAffine {d : ℕ} (z : Vec d) (L : ℝ) {E : Type u_1} [TopologicalSpace E] [ContinuousENorm E] (p : ENNReal) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (axisCubeNormalizedMeasure z L)) : (MeasureTheory.eLpNorm (fun (x : Vec d) => f (axisCubeAffine z L x)) p (MeasureTheory.volume.restrict (openCubeSet (originCube d 0)))).toReal = (MeasureTheory.eLpNorm f p (axisCubeNormalizedMeasure z L)).toReal

The corresponding real-valued normalized Lᵖ norms are affine invariant.

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeHarmonicPullback_grad {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) (x : Vec d) : (axisCubeHarmonicPullback z hL u).grad x = u.grad (axisCubeAffine z L x)

theorem HCPolySupport.CubeCalderonZygmund.memLp_axisCubeHarmonicPullback_grad_originCube_neg_nat_iff {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) (n : ℕ) (p : ENNReal) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => (axisCubeHarmonicPullback z hL u).grad x i) p (normalizedCubeMeasure (originCube d (-↑n))) ↔ MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) p (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

The fixed-depth MemLp transport specialized to a pulled-back harmonic gradient coordinate.

theorem HCPolySupport.CubeCalderonZygmund.eLpNorm_axisCubeHarmonicPullback_grad_originCube_neg_nat {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) (n : ℕ) (p : ENNReal) (i : Fin d) (hmem : MeasureTheory.MemLp (fun (x : Vec d) => (axisCubeHarmonicPullback z hL u).grad x i) p (normalizedCubeMeasure (originCube d (-↑n)))) : MeasureTheory.eLpNorm (fun (x : Vec d) => (axisCubeHarmonicPullback z hL u).grad x i) p (normalizedCubeMeasure (originCube d (-↑n))) = MeasureTheory.eLpNorm (fun (x : Vec d) => u.grad x i) p (axisCubeNormalizedMeasure (axisCubeConcentricDepthCorner z L n) (axisCubeConcentricDepthSide L n))

Exact fixed-depth norm transport specialized to a pulled-back harmonic gradient coordinate.

@[simp]

theorem HCPolySupport.CubeCalderonZygmund.axisCubeHarmonicPullback_toFun {d : ℕ} (z : Vec d) {L : ℝ} (hL : 0 < L) (u : H1Function (axisCube z L)) (x : Vec d) : (axisCubeHarmonicPullback z hL u).toFun x = L⁻¹ * u.toFun (axisCubeAffine z L x)