Normalized cube L^p and W^{1,p} quantities used later in the Besov layer.

The normalization is packaged through a probability measure on cubeSet Q, so the underlined norms match the note conventions without repeatedly rederiving factors of cubeVolume Q.

noncomputable def Homogenization.cubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure (Vec d)

Lebesgue measure restricted to a triadic cube.

Equations

• Homogenization.cubeMeasure Q = MeasureTheory.volume.restrict (Homogenization.cubeSet Q)

noncomputable def Homogenization.normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure (Vec d)

Lebesgue measure on a triadic cube normalized by its volume.

Equations

• Homogenization.normalizedCubeMeasure Q = ENNReal.ofReal (Homogenization.cubeVolume Q)⁻¹ • Homogenization.cubeMeasure Q

@[simp]

theorem Homogenization.cubeMeasure_apply_univ {d : ℕ} (Q : TriadicCube d) : (cubeMeasure Q) Set.univ = MeasureTheory.volume (cubeSet Q)

theorem Homogenization.cubeMeasure_apply_univ_toReal {d : ℕ} (Q : TriadicCube d) : ((cubeMeasure Q) Set.univ).toReal = cubeVolume Q

theorem Homogenization.cubeMeasure_apply_univ_ne_top {d : ℕ} (Q : TriadicCube d) : (cubeMeasure Q) Set.univ ≠ ⊤

theorem Homogenization.cubeMeasure_apply_univ_eq {d : ℕ} (Q : TriadicCube d) : (cubeMeasure Q) Set.univ = ENNReal.ofReal (cubeVolume Q)

@[simp]

theorem Homogenization.normalizedCubeMeasure_apply_univ {d : ℕ} (Q : TriadicCube d) : (normalizedCubeMeasure Q) Set.univ = 1

instance Homogenization.normalizedCubeMeasure.instIsFiniteMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (normalizedCubeMeasure Q)

theorem Homogenization.normalizedCubeMeasure_ne_zero {d : ℕ} (Q : TriadicCube d) : normalizedCubeMeasure Q ≠ 0

theorem Homogenization.cubeAverage_eq_integral_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeAverage Q f = ∫ (x : Vec d), f x ∂normalizedCubeMeasure Q

noncomputable def Homogenization.cubeLpNorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (f : Vec d → E) : ℝ

Real-valued Lp norm with respect to the normalized cube measure.

Equations

• Homogenization.cubeLpNorm Q p f = (MeasureTheory.eLpNorm f p (Homogenization.normalizedCubeMeasure Q)).toReal

noncomputable def Homogenization.cubeFluctuation {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : Vec d → ℝ

Scalar function minus its average over a triadic cube.

Equations

• Homogenization.cubeFluctuation Q f x = f x - Homogenization.cubeAverage Q f

theorem Homogenization.cubeAverage_sub_const_of_memLp_two {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) (c : ℝ) : (cubeAverage Q fun (x : Vec d) => f x - c) = cubeAverage Q f - c

theorem Homogenization.cubeFluctuation_sub_const_of_memLp_two {d : ℕ} (Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) (c : ℝ) : (cubeFluctuation Q fun (x : Vec d) => f x - c) = cubeFluctuation Q f

theorem Homogenization.cubeFluctuation_cubeFluctuation_of_memLp_two {d : ℕ} (R Q : TriadicCube d) {f : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure R)) : cubeFluctuation R (cubeFluctuation Q f) = cubeFluctuation R f

noncomputable def Homogenization.cubeW1pSeminorm {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (Du : Vec d → Vec d) : ℝ

Normalized cube Lp norm of a supplied gradient field.

Equations

• Homogenization.cubeW1pSeminorm Q p Du = Homogenization.cubeLpNorm Q p Du

noncomputable def Homogenization.cubeW1InfinityNorm {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ℝ

Maximum of the gradient L∞ norm and the scale-normalized function L∞ norm.

Equations

• Homogenization.cubeW1InfinityNorm Q u Du = max (Homogenization.cubeLpNorm Q ⊤ Du) ((Homogenization.cubeScaleFactor Q)⁻¹ * Homogenization.cubeLpNorm Q ⊤ u)

noncomputable def Homogenization.cubeW1pNorm {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (Du : Vec d → Vec d) : ℝ

Scale-normalized Sobolev norm on a triadic cube with the endpoint conventions for p.

Equations

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

theorem Homogenization.cubeLpNorm_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (f : Vec d → E) : 0 ≤ cubeLpNorm Q p f

@[simp]

theorem Homogenization.cubeLpNorm_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) : (cubeLpNorm Q p fun (x : Vec d) => 0) = 0

theorem Homogenization.cubeLpNorm_const {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (c : E) (hp : p ≠ 0) : (cubeLpNorm Q p fun (x : Vec d) => c) = ‖c‖

theorem Homogenization.cubeLpNorm_one_eq_integral_norm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (f : Vec d → E) (hf : MeasureTheory.AEStronglyMeasurable f (normalizedCubeMeasure Q)) : cubeLpNorm Q 1 f = ∫ (x : Vec d), ‖f x‖ ∂normalizedCubeMeasure Q

theorem Homogenization.cubeLpNorm_rpow_eq_cubeAverage_norm_rpow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (f : Vec d → E) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : cubeLpNorm Q p f ^ p.toReal = cubeAverage Q fun (x : Vec d) => ‖f x‖ ^ p.toReal

theorem Homogenization.cubeLpNorm_mul_le_mul_cubeLpNorm_of_holderConjugate {d : ℕ} (Q : TriadicCube d) (p q : ENNReal) (f g : Vec d → ℝ) [p.HolderConjugate q] (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g q (normalizedCubeMeasure Q)) : (cubeLpNorm Q 1 fun (x : Vec d) => f x * g x) ≤ cubeLpNorm Q p f * cubeLpNorm Q q g

theorem Homogenization.cubeLpNorm_mul_le_mul_cubeLpNorm_conjExponent {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (f g : Vec d → ℝ) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g p.conjExponent (normalizedCubeMeasure Q)) (hp : 1 ≤ p) : (cubeLpNorm Q 1 fun (x : Vec d) => f x * g x) ≤ cubeLpNorm Q p f * cubeLpNorm Q p.conjExponent g

theorem Homogenization.abs_cubeAverage_mul_le_mul_cubeLpNorm_of_holderConjugate {d : ℕ} (Q : TriadicCube d) (p q : ENNReal) (f g : Vec d → ℝ) [p.HolderConjugate q] (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g q (normalizedCubeMeasure Q)) : |cubeAverage Q fun (x : Vec d) => f x * g x| ≤ cubeLpNorm Q p f * cubeLpNorm Q q g

theorem Homogenization.abs_cubeAverage_mul_le_mul_cubeLpNorm_conjExponent {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (f g : Vec d → ℝ) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g p.conjExponent (normalizedCubeMeasure Q)) (hp : 1 ≤ p) : |cubeAverage Q fun (x : Vec d) => f x * g x| ≤ cubeLpNorm Q p f * cubeLpNorm Q p.conjExponent g

@[simp]

theorem Homogenization.cubeFluctuation_apply {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (x : Vec d) : cubeFluctuation Q f x = f x - cubeAverage Q f

@[simp]

theorem Homogenization.cubeFluctuation_const {d : ℕ} (Q : TriadicCube d) (c : ℝ) : (cubeFluctuation Q fun (x : Vec d) => c) = 0

theorem Homogenization.cubeFluctuation_zero {d : ℕ} (Q : TriadicCube d) : (cubeFluctuation Q fun (x : Vec d) => 0) = 0

@[simp]

theorem Homogenization.cubeAverage_cubeFluctuation {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeAverage Q (cubeFluctuation Q f) = 0

theorem Homogenization.cubeW1pSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (Du : Vec d → Vec d) : 0 ≤ cubeW1pSeminorm Q p Du

@[simp]

theorem Homogenization.cubeW1pSeminorm_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) : (cubeW1pSeminorm Q p fun (x : Vec d) => 0) = 0

@[simp]

theorem Homogenization.cubeW1pNorm_top {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (Du : Vec d → Vec d) : cubeW1pNorm Q ⊤ u Du = cubeW1InfinityNorm Q u Du

theorem Homogenization.cubeW1InfinityNorm_nonneg {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (Du : Vec d → Vec d) : 0 ≤ cubeW1InfinityNorm Q u Du

@[simp]

theorem Homogenization.cubeW1InfinityNorm_zero {d : ℕ} (Q : TriadicCube d) : (cubeW1InfinityNorm Q (fun (x : Vec d) => 0) fun (x : Vec d) => 0) = 0

theorem Homogenization.cubeW1pNorm_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (Du : Vec d → Vec d) : 0 ≤ cubeW1pNorm Q p u Du

@[simp]

theorem Homogenization.cubeW1pNorm_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) : (cubeW1pNorm Q p (fun (x : Vec d) => 0) fun (x : Vec d) => 0) = 0