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

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

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

Note-normalized full positive q = 2 Besov norm for vector fields.

Equations

• HCPolySupport.cubeBesovPositiveVectorNormTwo Q s F = √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec Q F)) + HCPolySupport.cubeBesovPositiveVectorSeminormTwo Q s F

Overlapping positive Besov norm

The disjoint descendant norm above is useful elsewhere in Chapter 3, but it is not the right endpoint for the classical K(L²,H¹) interpolation route: it does not see jumps across the boundaries of the active triadic partition. The corrected norm below tests oscillation on overlapping cubes. At depth j, the centers lie on the grid one generation finer than the cube size.

noncomputable def HCPolySupport.overlapCubeScaleFactor {d : ℕ} (S : TriadicCube d) : ℝ

Side length of the overlapping cube centered at the fine-grid cube S. If S has scale k - 1, this overlapping cube has side length 3^k.

Equations

• HCPolySupport.overlapCubeScaleFactor S = 3 * HCPolySupport.cubeScaleFactor S

theorem HCPolySupport.overlapCubeScaleFactor_pos {d : ℕ} (S : TriadicCube d) : 0 < overlapCubeScaleFactor S

theorem HCPolySupport.overlapCubeScaleFactor_nonneg {d : ℕ} (S : TriadicCube d) : 0 ≤ overlapCubeScaleFactor S

def HCPolySupport.overlapCubeSet {d : ℕ} (S : TriadicCube d) : Set (Vec d)

The half-open overlapping cube centered at cubeCenter S with side length 3 * cubeScaleFactor S.

Equations

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

def HCPolySupport.openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : Set (Vec d)

The open overlapping cube with the same center and side length as overlapCubeSet. This is the analytic domain used by the local H¹ Poincare estimate.

Equations

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

theorem HCPolySupport.measurableSet_coord_overlapHalfOpenStrip {d : ℕ} (i : Fin d) (a b : ℝ) : MeasurableSet {x : Vec d | a ≤ x i ∧ x i < b}

theorem HCPolySupport.measurableSet_coord_overlapOpenStrip {d : ℕ} (i : Fin d) (a b : ℝ) : MeasurableSet {x : Vec d | a < x i ∧ x i < b}

theorem HCPolySupport.measurableSet_overlapCubeSet {d : ℕ} (S : TriadicCube d) : MeasurableSet (overlapCubeSet S)

theorem HCPolySupport.measurableSet_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : MeasurableSet (openOverlapCubeSet S)

theorem HCPolySupport.isOpen_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : IsOpen (openOverlapCubeSet S)

theorem HCPolySupport.overlapCubeSet_eq_pi_Ico {d : ℕ} (S : TriadicCube d) : overlapCubeSet S = Set.univ.pi fun (i : Fin d) => Set.Ico ((↑(S.index i) - 3 / 2) * cubeScaleFactor S) ((↑(S.index i) + 3 / 2) * cubeScaleFactor S)

theorem HCPolySupport.openOverlapCubeSet_eq_pi_Ioo {d : ℕ} (S : TriadicCube d) : openOverlapCubeSet S = Set.univ.pi fun (i : Fin d) => Set.Ioo ((↑(S.index i) - 3 / 2) * cubeScaleFactor S) ((↑(S.index i) + 3 / 2) * cubeScaleFactor S)

theorem HCPolySupport.overlapCubeSet_ae_eq_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : overlapCubeSet S =ᵐ[MeasureTheory.volume] openOverlapCubeSet S

theorem HCPolySupport.volume_restrict_overlapCubeSet_eq_volume_restrict_openOverlapCubeSet {d : ℕ} (S : TriadicCube d) : MeasureTheory.volume.restrict (overlapCubeSet S) = MeasureTheory.volume.restrict (openOverlapCubeSet S)

theorem HCPolySupport.integrableOn_overlapCubeSet_iff_integrableOn_openOverlapCubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {S : TriadicCube d} {f : Vec d → E} : MeasureTheory.IntegrableOn f (overlapCubeSet S) MeasureTheory.volume ↔ MeasureTheory.IntegrableOn f (openOverlapCubeSet S) MeasureTheory.volume

theorem HCPolySupport.setIntegral_overlapCubeSet_eq_setIntegral_openOverlapCubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {S : TriadicCube d} {f : Vec d → E} : ∫ (x : Vec d) in overlapCubeSet S, f x = ∫ (x : Vec d) in openOverlapCubeSet S, f x

theorem HCPolySupport.openOverlapCubeSet_subset_overlapCubeSet {d : ℕ} (S : TriadicCube d) : openOverlapCubeSet S ⊆ overlapCubeSet S

theorem HCPolySupport.interior_cubeSet_eq_openCubeSet {d : ℕ} (Q : TriadicCube d) : interior (cubeSet Q) = openCubeSet Q

theorem HCPolySupport.overlapCubeScaleFactor_eq_cubeScaleFactor_originCube_succ {d : ℕ} (S : TriadicCube d) : overlapCubeScaleFactor S = cubeScaleFactor (originCube d (S.scale + 1))

theorem HCPolySupport.openOverlapCubeSet_eq_translateSet_smul_originCube_zero {d : ℕ} (S : TriadicCube d) : openOverlapCubeSet S = translateSet (cubeCenter S) (overlapCubeScaleFactor S • openCubeSet (originCube d 0))

noncomputable def HCPolySupport.openOverlapCubeMeanZeroH1CoerciveEstimate {d : ℕ} (S : TriadicCube d) : H1CoerciveEstimate (openOverlapCubeSet S)

Scale-correct mean-zero H¹ coercive estimate on an open overlap cube, obtained by dilating the unit centered cube estimate by the overlap side length and translating to the overlap center.

Equations

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

@[simp]

theorem HCPolySupport.openOverlapCubeMeanZeroH1CoerciveEstimate_constant {d : ℕ} (S : TriadicCube d) : (openOverlapCubeMeanZeroH1CoerciveEstimate S).constantValue = overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue

def HCPolySupport.middleChildCube {d : ℕ} (Q : TriadicCube d) : TriadicCube d

The middle child of a triadic cube. It is the child whose center agrees with the center of the parent.

Equations

• HCPolySupport.middleChildCube Q = { scale := Q.scale - 1, index := fun (i : Fin d) => 3 * Q.index i }

theorem HCPolySupport.middleChildCube_mem_childCubes {d : ℕ} (Q : TriadicCube d) : middleChildCube Q ∈ childCubes Q

theorem HCPolySupport.overlapCubeSet_middleChildCube_eq_cubeSet {d : ℕ} (Q : TriadicCube d) : overlapCubeSet (middleChildCube Q) = cubeSet Q

theorem HCPolySupport.overlapCubeSet_middleChildCube_subset_cubeSet {d : ℕ} (Q : TriadicCube d) : overlapCubeSet (middleChildCube Q) ⊆ cubeSet Q

def HCPolySupport.middleDescendant {d : ℕ} (Q : TriadicCube d) : ℕ → TriadicCube d

The iterated middle descendant at depth n.

Equations

• HCPolySupport.middleDescendant Q 0 = Q
• HCPolySupport.middleDescendant Q n.succ = HCPolySupport.middleChildCube (HCPolySupport.middleDescendant Q n)

theorem HCPolySupport.middleDescendant_mem_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (n : ℕ) : middleDescendant Q n ∈ descendantsAtDepth Q n

theorem HCPolySupport.overlapCubeSet_middleDescendant_succ_subset_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) : overlapCubeSet (middleDescendant Q (j + 1)) ⊆ cubeSet Q

theorem HCPolySupport.middleChildCube_injective {d : ℕ} : Function.Injective middleChildCube

theorem HCPolySupport.cubeColor_index_add_three_le_of_lt {d : ℕ} {R S : TriadicCube d} {i : Fin d} (hcolor : cubeColor R = cubeColor S) (hlt : R.index i < S.index i) : R.index i + 3 ≤ S.index i

theorem HCPolySupport.disjoint_overlapCubeSet_of_scale_eq_of_cubeColor_eq_of_ne {d : ℕ} {R S : TriadicCube d} (hscale : R.scale = S.scale) (hcolor : cubeColor R = cubeColor S) (hneq : R ≠ S) : Disjoint (overlapCubeSet R) (overlapCubeSet S)

noncomputable def HCPolySupport.overlapCubeVolume {d : ℕ} (S : TriadicCube d) : ℝ

Volume of an overlapping cube.

Equations

• HCPolySupport.overlapCubeVolume S = HCPolySupport.overlapCubeScaleFactor S ^ d

theorem HCPolySupport.overlapCubeVolume_pos {d : ℕ} (S : TriadicCube d) : 0 < overlapCubeVolume S

theorem HCPolySupport.overlapCubeVolume_nonneg {d : ℕ} (S : TriadicCube d) : 0 ≤ overlapCubeVolume S

@[simp]

theorem HCPolySupport.volume_overlapCubeSet_toReal {d : ℕ} (S : TriadicCube d) : (MeasureTheory.volume (overlapCubeSet S)).toReal = overlapCubeVolume S

@[simp]

theorem HCPolySupport.volume_openOverlapCubeSet_toReal {d : ℕ} (S : TriadicCube d) : (MeasureTheory.volume (openOverlapCubeSet S)).toReal = overlapCubeVolume S

theorem HCPolySupport.volume_overlapCubeSet_lt_top {d : ℕ} (S : TriadicCube d) : MeasureTheory.volume (overlapCubeSet S) < ⊤

theorem HCPolySupport.volume_openOverlapCubeSet_lt_top {d : ℕ} (S : TriadicCube d) : MeasureTheory.volume (openOverlapCubeSet S) < ⊤

instance HCPolySupport.openOverlapCubeSet.instIsFiniteMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (openOverlapCubeSet S))

theorem HCPolySupport.openOverlapCubeMeanZero_valueL2Norm_le {d : ℕ} (S : TriadicCube d) (u : H1Function (openOverlapCubeSet S)) : u.toMeanZero.valueL2Norm ≤ overlapCubeScaleFactor S * (originCubeMeanZeroH1CoerciveEstimate d 0).constantValue * ‖u.gradToVectorL2‖

noncomputable def HCPolySupport.overlapCubeMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.Measure (Vec d)

Unnormalized measure on an overlapping cube.

Equations

• HCPolySupport.overlapCubeMeasure S = MeasureTheory.volume.restrict (HCPolySupport.overlapCubeSet S)

noncomputable def HCPolySupport.normalizedOverlapCubeMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.Measure (Vec d)

Normalized measure on an overlapping cube.

Equations

• HCPolySupport.normalizedOverlapCubeMeasure S = ENNReal.ofReal (HCPolySupport.overlapCubeVolume S)⁻¹ • HCPolySupport.overlapCubeMeasure S

theorem HCPolySupport.lintegral_normalizedCubeMeasure_eq {d : ℕ} (Q : TriadicCube d) (f : Vec d → ENNReal) : ∫⁻ (x : Vec d), f x ∂normalizedCubeMeasure Q = ENNReal.ofReal (cubeVolume Q)⁻¹ * ∫⁻ (x : Vec d) in cubeSet Q, f x

theorem HCPolySupport.ae_openCubeSet_normalizedCubeMeasure {d : ℕ} (Q : TriadicCube d) : ∀ᵐ (x : Vec d) ∂normalizedCubeMeasure Q, x ∈ openCubeSet Q

theorem HCPolySupport.lintegral_normalizedOverlapCubeMeasure_eq {d : ℕ} (S : TriadicCube d) (f : Vec d → ENNReal) : ∫⁻ (x : Vec d), f x ∂normalizedOverlapCubeMeasure S = ENNReal.ofReal (overlapCubeVolume S)⁻¹ * ∫⁻ (x : Vec d) in overlapCubeSet S, f x

@[simp]

theorem HCPolySupport.overlapCubeMeasure_apply_univ {d : ℕ} (S : TriadicCube d) : (overlapCubeMeasure S) Set.univ = MeasureTheory.volume (overlapCubeSet S)

theorem HCPolySupport.overlapCubeMeasure_apply_univ_toReal {d : ℕ} (S : TriadicCube d) : ((overlapCubeMeasure S) Set.univ).toReal = overlapCubeVolume S

theorem HCPolySupport.overlapCubeMeasure_apply_univ_ne_top {d : ℕ} (S : TriadicCube d) : (overlapCubeMeasure S) Set.univ ≠ ⊤

theorem HCPolySupport.overlapCubeMeasure_apply_univ_eq {d : ℕ} (S : TriadicCube d) : (overlapCubeMeasure S) Set.univ = ENNReal.ofReal (overlapCubeVolume S)

@[simp]

theorem HCPolySupport.normalizedOverlapCubeMeasure_apply_univ {d : ℕ} (S : TriadicCube d) : (normalizedOverlapCubeMeasure S) Set.univ = 1

instance HCPolySupport.normalizedOverlapCubeMeasure.instIsFiniteMeasure {d : ℕ} (S : TriadicCube d) : MeasureTheory.IsFiniteMeasure (normalizedOverlapCubeMeasure S)

theorem HCPolySupport.normalizedOverlapCubeMeasure_ne_zero {d : ℕ} (S : TriadicCube d) : normalizedOverlapCubeMeasure S ≠ 0