Coarse-graining support: Support.Multiscale.NormalizedNorms

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

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 HCPolySupport.cubeMeasure {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure (Vec d)

Lebesgue measure restricted to the cube.

Equations

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

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

Cube Lebesgue measure divided by the cube's volume.

Equations

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

The real value of the Lᵖ seminorm for normalized cube measure, with infinity mapped to zero.

Equations

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

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

The function obtained by subtracting its average over the cube.

Equations

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

theorem HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.cubeW1pSeminorm {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (Du : Vec d → Vec d) : ℝ

The normalized cube Lᵖ norm of the supplied gradient field.

Equations

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

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

The maximum of the gradient's L∞ norm and the value's L∞ norm divided by side length.

Equations

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

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

The scale-normalized Sobolev norm combining gradient and value Lᵖ norms; it is zero for p = 0 and uses the maximum formula for p = ∞.

Equations

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

theorem HCPolySupport.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 HCPolySupport.cubeLpNorm_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) : (cubeLpNorm Q p fun (x : Vec d) => 0) = 0

theorem HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.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 HCPolySupport.cubeFluctuation_apply {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (x : Vec d) : cubeFluctuation Q f x = f x - cubeAverage Q f

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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