Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.OverlapFluctuation

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

noncomputable def HCPolySupport.overlapCentersAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) : ℝ

Average over the overlapping centers at a fixed depth.

Equations

• HCPolySupport.overlapCentersAverage Q j F = (↑(HCPolySupport.overlapCentersAtDepth Q j).card)⁻¹ * (HCPolySupport.overlapCentersAtDepth Q j).sum F

theorem HCPolySupport.overlapCentersAverage_add {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F G : TriadicCube d → ℝ) : (overlapCentersAverage Q j fun (S : TriadicCube d) => F S + G S) = overlapCentersAverage Q j F + overlapCentersAverage Q j G

theorem HCPolySupport.overlapCentersAverage_mul_left {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) : (overlapCentersAverage Q j fun (S : TriadicCube d) => c * F S) = c * overlapCentersAverage Q j F

theorem HCPolySupport.overlapCentersAverage_le_overlapCentersAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F G : TriadicCube d → ℝ} (hFG : ∀ S ∈ overlapCentersAtDepth Q j, F S ≤ G S) : overlapCentersAverage Q j F ≤ overlapCentersAverage Q j G

theorem HCPolySupport.overlapCentersAverage_const_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (hD : (overlapCentersAtDepth Q j).Nonempty) : (overlapCentersAverage Q j fun (x : TriadicCube d) => c) = c

theorem HCPolySupport.overlapCentersAverage_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) : (overlapCentersAverage Q j fun (x : TriadicCube d) => c) = c

theorem HCPolySupport.overlapCentersAverage_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) (hF : ∀ S ∈ overlapCentersAtDepth Q j, 0 ≤ F S) : 0 ≤ overlapCentersAverage Q j F

theorem HCPolySupport.overlapCentersAverage_L2_sum_le_sum_overlapCentersAverage_L2 {d : ℕ} {ι : Type u_1} (Q : TriadicCube d) (j : ℕ) (s : Finset ι) (A : TriadicCube d → ι → ℝ) (hA : ∀ S ∈ overlapCentersAtDepth Q j, ∀ i ∈ s, 0 ≤ A S i) : (overlapCentersAverage Q j fun (S : TriadicCube d) => (∑ i ∈ s, A S i) ^ 2) ^ (1 / 2) ≤ ∑ i ∈ s, (overlapCentersAverage Q j fun (S : TriadicCube d) => A S i ^ 2) ^ (1 / 2)

theorem HCPolySupport.overlapCentersAverage_lintegral_rpow_enorm_two_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (Q : TriadicCube d) (j : ℕ) (R : Vec d → E) (hR : MeasureTheory.MemLp R 2 (normalizedCubeMeasure Q)) (hRloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp R 2 (normalizedOverlapCubeMeasure S)) : (overlapCentersAverage Q j fun (S : TriadicCube d) => (∫⁻ (x : Vec d), ‖R x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S).toReal) ≤ 3 ^ d * (∫⁻ (x : Vec d), ‖R x‖ₑ ^ 2 ∂normalizedCubeMeasure Q).toReal

noncomputable def HCPolySupport.overlapCubeFluctuationVec {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) : Vec d → Vec d

Vector fluctuation around the overlapping-cube average.

Equations

• HCPolySupport.overlapCubeFluctuationVec S u x = u x - HCPolySupport.overlapCubeAverageVec S u

@[simp]

theorem HCPolySupport.overlapCubeFluctuationVec_zero {d : ℕ} (S : TriadicCube d) : overlapCubeFluctuationVec S 0 = 0

theorem HCPolySupport.overlapCentersAtDepth_average_lintegral_ofReal_vecNormSq_fluctuation_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (h : Vec d → Vec d) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S ≤ ↑(Fintype.card (Fin d)) * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ‖overlapCubeFluctuationVec S h x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S)

theorem HCPolySupport.overlapCubeAverage_add_of_memLp_two {d : ℕ} (S : TriadicCube d) {f g : Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (normalizedOverlapCubeMeasure S)) (hg : MeasureTheory.MemLp g 2 (normalizedOverlapCubeMeasure S)) : (overlapCubeAverage S fun (x : Vec d) => f x + g x) = overlapCubeAverage S f + overlapCubeAverage S g

theorem HCPolySupport.overlapCubeAverageVec_add_of_memLp_two {d : ℕ} (S : TriadicCube d) {u v : Vec d → Vec d} (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) (hv : MeasureTheory.MemLp v 2 (normalizedOverlapCubeMeasure S)) : (overlapCubeAverageVec S fun (x : Vec d) => u x + v x) = overlapCubeAverageVec S u + overlapCubeAverageVec S v

theorem HCPolySupport.memLp_overlapCubeFluctuationVec {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : MeasureTheory.MemLp (overlapCubeFluctuationVec S u) 2 (normalizedOverlapCubeMeasure S)

theorem HCPolySupport.overlapCubeFluctuationVec_add_of_memLp_two {d : ℕ} (S : TriadicCube d) {u v : Vec d → Vec d} (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) (hv : MeasureTheory.MemLp v 2 (normalizedOverlapCubeMeasure S)) : (overlapCubeFluctuationVec S fun (x : Vec d) => u x + v x) = fun (x : Vec d) => overlapCubeFluctuationVec S u x + overlapCubeFluctuationVec S v x

theorem HCPolySupport.overlapCubeLpNorm_two_overlapCubeFluctuationVec_le_two_mul_overlapCubeLpNorm_two {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S u) ≤ 2 * overlapCubeLpNorm S 2 u

theorem HCPolySupport.sq_overlapCubeLpNorm_fluctuation_le_four_pointwiseBound {d : ℕ} {S : TriadicCube d} {u : Vec d → Vec d} {B : ℝ} (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) (hB : 0 ≤ B) (hpoint : ∀ x ∈ overlapCubeSet S, vecNormSq (u x) ≤ B) : overlapCubeLpNorm S 2 (overlapCubeFluctuationVec S u) ^ 2 ≤ 4 * B

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

Depth-j overlapping positive q = 2 square average.

Equations

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

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ cubeBesovOverlappingPositiveVectorDepthAverage Q u j

theorem HCPolySupport.toReal_overlapCentersAtDepth_average_lintegral_fluctuation_eq_depthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (hfin : ∀ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ‖overlapCubeFluctuationVec S u x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S ≠ ⊤) (hmeas : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.AEStronglyMeasurable u (normalizedOverlapCubeMeasure S)) : ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ‖overlapCubeFluctuationVec S u x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S).toReal = cubeBesovOverlappingPositiveVectorDepthAverage Q u j

theorem HCPolySupport.lintegral_overlapCubeFluctuationVec_rpow_enorm_two_ne_top {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : ∫⁻ (x : Vec d), ‖overlapCubeFluctuationVec S u x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S ≠ ⊤

theorem HCPolySupport.overlapCentersAtDepth_average_lintegral_fluctuation_ne_top {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (hu : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ‖overlapCubeFluctuationVec S u x‖ₑ ^ 2 ∂normalizedOverlapCubeMeasure S ≠ ⊤

theorem HCPolySupport.overlapCentersAtDepth_average_lintegral_ofReal_vecNormSq_fluctuation_ne_top {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (hu : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (u x - overlapCubeAverageVec S u)) ∂normalizedOverlapCubeMeasure S ≠ ⊤

theorem HCPolySupport.residualEuclideanOverlapBound_ne_top_of_memLp_overlap {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j M : ℕ) (hu : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) : ↑M * 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (u x - overlapCubeAverageVec S u)) ∂normalizedOverlapCubeMeasure S) ≠ ⊤