Coarse-graining support: Support.Deterministic.ConstantCoefficientDirichletBesov.PositiveNorm

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

theorem HCPolySupport.aemeasurable_overlapCubeResidualIndicator_of_memLp {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {h : Vec d → Vec d} (hS : S ∈ overlapCentersAtDepth Q j) (hh : MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : AEMeasurable ((overlapCubeSet S).indicator fun (y : Vec d) => ENNReal.ofReal (vecNormSq (h y - overlapCubeAverageVec S h))) (MeasureTheory.volume.restrict (cubeSet Q))

theorem HCPolySupport.aemeasurable_overlapCubeCoordResidualIndicator_of_memLp {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {h : Vec d → Vec d} (i : Fin d) (hS : S ∈ overlapCentersAtDepth Q j) (hh : MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : AEMeasurable ((overlapCubeSet S).indicator fun (y : Vec d) => ENNReal.ofReal ((h y i - overlapCubeAverageVec S h i) ^ 2)) (MeasureTheory.volume.restrict (cubeSet Q))

Coordinate version of the closed-overlap fluctuation indicator measurability lemma.

theorem HCPolySupport.lintegral_sum_coord_fluctuation_indicator_le_vector_average {d : ℕ} (Q : TriadicCube d) (h : Vec d → Vec d) (j : ℕ) (i : Fin d) (hloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp h 2 (normalizedOverlapCubeMeasure S)) : ∫⁻ (x : Vec d), ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (fun (y : Vec d) => ENNReal.ofReal ((h y i - overlapCubeAverageVec S h i) ^ 2)) x ∂normalizedCubeMeasure Q ≤ 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), ENNReal.ofReal (vecNormSq (h x - overlapCubeAverageVec S h)) ∂normalizedOverlapCubeMeasure S)

Integrated coordinate fluctuation indicators are controlled by the vector-valued overlap fluctuation average.

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_add_le {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (j : ℕ) (hu : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedOverlapCubeMeasure S)) (hv : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp v 2 (normalizedOverlapCubeMeasure S)) : cubeBesovOverlappingPositiveVectorDepthAverage Q (fun (x : Vec d) => u x + v x) j ≤ 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q u j + 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q v j

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage_residual_le {d : ℕ} (Q : TriadicCube d) (R : Vec d → Vec d) (j : ℕ) (hR : MeasureTheory.MemLp R 2 (normalizedCubeMeasure Q)) (hRloc : ∀ S ∈ overlapCentersAtDepth Q j, MeasureTheory.MemLp R 2 (normalizedOverlapCubeMeasure S)) : cubeBesovOverlappingPositiveVectorDepthAverage Q R j ≤ 4 * 3 ^ d * cubeLpNorm Q 2 R ^ 2

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

Depth-j overlapping positive q = 2 seminorm.

Equations

• HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j = Real.rpow 3 (s * ↑j) * √(HCPolySupport.cubeBesovOverlappingPositiveVectorDepthAverage Q u j)

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2 = Real.rpow 3 (s * ↑j) ^ 2 * cubeBesovOverlappingPositiveVectorDepthAverage Q u j

noncomputable def HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : ℝ

Finite-depth overlapping positive q = 2 seminorm.

Equations

• HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u = √(∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2)

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : 0 ≤ cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.sq_cubeBesovOverlappingPositiveVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2

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

Full overlapping positive q = 2 seminorm.

Equations

• HCPolySupport.cubeBesovOverlappingPositiveVectorSeminormTwo Q s u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorSeminormTwo_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u ≤ B) : cubeBesovOverlappingPositiveVectorSeminormTwo Q s u ≤ B

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorPartialSeminormTwo_le_seminorm_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)) (N : ℕ) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u ≤ cubeBesovOverlappingPositiveVectorSeminormTwo Q s u

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorSeminormTwo_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)) : 0 ≤ cubeBesovOverlappingPositiveVectorSeminormTwo Q s u

noncomputable def HCPolySupport.cubeBesovOverlappingPositiveVectorNormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) : ℝ

Corrected full positive q = 2 Besov norm for vector fields, using overlapping cubes at each depth.

Equations

• HCPolySupport.cubeBesovOverlappingPositiveVectorNormTwo Q s F = √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec Q F)) + HCPolySupport.cubeBesovOverlappingPositiveVectorSeminormTwo Q s F

theorem HCPolySupport.cubeBesovOverlappingPositiveVectorNormTwo_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (F : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N F)) : 0 ≤ cubeBesovOverlappingPositiveVectorNormTwo Q s F

structure HCPolySupport.CubeVectorOverlappingBesovHRegularity {d : ℕ} (Q : TriadicCube d) (s : ℝ) (g : Vec d → Vec d) : Prop

Corrected H^s regularity package for the overlapping positive norm.

• memLp : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)
• partialSeminorms_bddAbove : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N g)

theorem HCPolySupport.CubeVectorOverlappingBesovHRegularity.partialSeminorm_le_seminorm {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : CubeVectorOverlappingBesovHRegularity Q s g) (N : ℕ) : cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N g ≤ cubeBesovOverlappingPositiveVectorSeminormTwo Q s g

theorem HCPolySupport.CubeVectorOverlappingBesovHRegularity.seminorm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : CubeVectorOverlappingBesovHRegularity Q s g) : 0 ≤ cubeBesovOverlappingPositiveVectorSeminormTwo Q s g

theorem HCPolySupport.CubeVectorOverlappingBesovHRegularity.norm_nonneg {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : CubeVectorOverlappingBesovHRegularity Q s g) : 0 ≤ cubeBesovOverlappingPositiveVectorNormTwo Q s g