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

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

noncomputable def HCPolySupport.overlapCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : Finset (TriadicCube d)

Fine-grid centers used by the overlapping norm at depth j.

The centers are descendants one generation below the cube scale. We retain only those centers whose overlapping cube lies inside the parent cube; this keeps the local Dirichlet theorem from sampling outside the cube where the solution representative has no Sobolev control.

Equations

• HCPolySupport.overlapCentersAtDepth Q j = {S ∈ HCPolySupport.descendantsAtDepth Q (j + 1) | HCPolySupport.overlapCubeSet S ⊆ HCPolySupport.cubeSet Q}

theorem HCPolySupport.mem_overlapCentersAtDepth_iff {d : ℕ} {Q S : TriadicCube d} {j : ℕ} : S ∈ overlapCentersAtDepth Q j ↔ S ∈ descendantsAtDepth Q (j + 1) ∧ overlapCubeSet S ⊆ cubeSet Q

theorem HCPolySupport.mem_descendantsAtDepth_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : S ∈ descendantsAtDepth Q (j + 1)

theorem HCPolySupport.overlapCubeSet_subset_cubeSet_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeSet S ⊆ cubeSet Q

theorem HCPolySupport.openOverlapCubeSet_subset_openCubeSet_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : openOverlapCubeSet S ⊆ openCubeSet Q

theorem HCPolySupport.memLp_normalizedOverlapCubeMeasure_of_memLp_normalizedCubeMeasure {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {Q S : TriadicCube d} {j : ℕ} {p : ENNReal} {f : Vec d → E} (hS : S ∈ overlapCentersAtDepth Q j) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (normalizedOverlapCubeMeasure S)

theorem HCPolySupport.overlapCubeScaleFactor_eq_cubeScaleFactor_div_pow_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeScaleFactor S = cubeScaleFactor Q / 3 ^ j

theorem HCPolySupport.inv_cubeScaleFactor_eq_three_mul_inv_depthScale_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : (cubeScaleFactor S)⁻¹ = 3 * (cubeScaleFactor Q / 3 ^ j)⁻¹

theorem HCPolySupport.overlapCubeVolume_eq_cubeVolume_div_pow_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : overlapCubeVolume S = cubeVolume Q / (3 ^ d) ^ j

theorem HCPolySupport.middleDescendant_succ_mem_overlapCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : middleDescendant Q (j + 1) ∈ overlapCentersAtDepth Q j

theorem HCPolySupport.overlapCentersAtDepth_nonempty {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (overlapCentersAtDepth Q j).Nonempty

theorem HCPolySupport.overlapCentersAtDepth_card_pos {d : ℕ} (Q : TriadicCube d) (j : ℕ) : 0 < (overlapCentersAtDepth Q j).card

theorem HCPolySupport.one_le_overlapCentersAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) : 1 ≤ (overlapCentersAtDepth Q j).card

theorem HCPolySupport.overlapCentersAtDepth_card_ne_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (overlapCentersAtDepth Q j).card ≠ 0

theorem HCPolySupport.overlapCentersAtDepth_card_real_ne_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) : ↑(overlapCentersAtDepth Q j).card ≠ 0

theorem HCPolySupport.overlapCentersAtDepth_card_le_descendantsAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (overlapCentersAtDepth Q j).card ≤ (descendantsAtDepth Q (j + 1)).card

theorem HCPolySupport.overlapCentersAtDepth_card_le_pow {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (overlapCentersAtDepth Q j).card ≤ (3 ^ d) ^ (j + 1)

theorem HCPolySupport.middleChildCube_mem_overlapCentersAtDepth_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) : middleChildCube R ∈ overlapCentersAtDepth Q j

theorem HCPolySupport.exists_mem_overlapCentersAtDepth_of_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} (j : ℕ) (hx : x ∈ cubeSet Q) : ∃ S ∈ overlapCentersAtDepth Q j, x ∈ overlapCubeSet S

theorem HCPolySupport.cubeSet_subset_iUnion_overlapCentersAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) : cubeSet Q ⊆ ⋃ S ∈ ↑(overlapCentersAtDepth Q j), overlapCubeSet S

theorem HCPolySupport.descendantsAtDepth_card_le_overlapCentersAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (descendantsAtDepth Q j).card ≤ (overlapCentersAtDepth Q j).card

theorem HCPolySupport.pow_le_overlapCentersAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) : (3 ^ d) ^ j ≤ (overlapCentersAtDepth Q j).card

theorem HCPolySupport.cubeVolume_le_card_mul_overlapCubeVolume_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : cubeVolume Q ≤ ↑(overlapCentersAtDepth Q j).card * overlapCubeVolume S

theorem HCPolySupport.card_mul_overlapCubeVolume_le_pow_mul_cubeVolume_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : ↑(overlapCentersAtDepth Q j).card * overlapCubeVolume S ≤ 3 ^ d * cubeVolume Q

theorem HCPolySupport.inv_cubeVolume_le_pow_mul_inv_card_mul_inv_overlapCubeVolume_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : (cubeVolume Q)⁻¹ ≤ 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * (overlapCubeVolume S)⁻¹)

theorem HCPolySupport.inv_card_mul_inv_overlapCubeVolume_le_inv_cubeVolume_of_mem_overlapCentersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * (overlapCubeVolume S)⁻¹ ≤ (cubeVolume Q)⁻¹

theorem HCPolySupport.inv_card_mul_ofReal_inv_overlapCubeVolume_le_ofReal_inv_cubeVolume {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * ENNReal.ofReal (overlapCubeVolume S)⁻¹ ≤ ENNReal.ofReal (cubeVolume Q)⁻¹

theorem HCPolySupport.ofReal_inv_cubeVolume_le_pow_mul_inv_card_mul_ofReal_inv_overlapCubeVolume {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ overlapCentersAtDepth Q j) : ENNReal.ofReal (cubeVolume Q)⁻¹ ≤ 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ENNReal.ofReal (overlapCubeVolume S)⁻¹)

theorem HCPolySupport.overlapCentersAtDepth_lintegral_sum_indicator_normalizedCubeMeasure_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) {f : TriadicCube d → Vec d → ENNReal} (hfQ : ∀ S ∈ overlapCentersAtDepth Q j, AEMeasurable ((overlapCubeSet S).indicator (f S)) (MeasureTheory.volume.restrict (cubeSet Q))) : ∫⁻ (x : Vec d), ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator (f S) x ∂normalizedCubeMeasure Q ≤ 3 ^ d * ((↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), f S x ∂normalizedOverlapCubeMeasure S)

Reverse normalized integral comparison for families indexed by retained overlap centers. Integrating a sum of overlap-supported nonnegative fields on the parent normalized cube is controlled by the average of the normalized overlap-cube integrals, with only a dimension constant.

noncomputable def HCPolySupport.overlapCentersAtDepthContaining {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : Finset (TriadicCube d)

The overlap centers at depth j whose overlap cube contains x.

Equations

• HCPolySupport.overlapCentersAtDepthContaining Q j x = {S ∈ HCPolySupport.overlapCentersAtDepth Q j | x ∈ HCPolySupport.overlapCubeSet S}

theorem HCPolySupport.mem_overlapCentersAtDepthContaining_iff {d : ℕ} {Q S : TriadicCube d} {j : ℕ} {x : Vec d} : S ∈ overlapCentersAtDepthContaining Q j x ↔ S ∈ overlapCentersAtDepth Q j ∧ x ∈ overlapCubeSet S

theorem HCPolySupport.cubeColor_injOn_overlapCentersAtDepthContaining {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : Set.InjOn cubeColor ↑(overlapCentersAtDepthContaining Q j x)

theorem HCPolySupport.overlapCentersAtDepthContaining_card_le_pow {d : ℕ} (Q : TriadicCube d) (j : ℕ) (x : Vec d) : (overlapCentersAtDepthContaining Q j x).card ≤ 3 ^ d

theorem HCPolySupport.overlapCentersAtDepth_sum_indicator_le_mul_cubeSet_indicator {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ENNReal) : (fun (x : Vec d) => ∑ S ∈ overlapCentersAtDepth Q j, (overlapCubeSet S).indicator f x) ≤ fun (x : Vec d) => 3 ^ d * (cubeSet Q).indicator f x

Pointwise finite-overlap bound for the overlapping cubes. This is the indicator form of the multiplicity estimate: inside the parent cube at most 3^d overlap cubes contain a point, and outside the parent cube none of the retained overlap cubes contribute.

theorem HCPolySupport.overlapCentersAtDepth_sum_setLIntegral_le_mul_setLIntegral_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) {f : Vec d → ENNReal} (hfQ : AEMeasurable f (MeasureTheory.volume.restrict (cubeSet Q))) (hfS : ∀ S ∈ overlapCentersAtDepth Q j, AEMeasurable f (MeasureTheory.volume.restrict (overlapCubeSet S))) : ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d) in overlapCubeSet S, f x ≤ 3 ^ d * ∫⁻ (x : Vec d) in cubeSet Q, f x

Integrated finite-overlap bound for nonnegative functions on the retained overlap cubes. This is the measure-level form of the geometry API used by the overlapping Besov endpoint.

theorem HCPolySupport.overlapCentersAtDepth_average_lintegral_normalizedOverlapCubeMeasure_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) {f : Vec d → ENNReal} (hfQ : AEMeasurable f (MeasureTheory.volume.restrict (cubeSet Q))) (hfS : ∀ S ∈ overlapCentersAtDepth Q j, AEMeasurable f (MeasureTheory.volume.restrict (overlapCubeSet S))) : (↑(overlapCentersAtDepth Q j).card)⁻¹ * ∑ S ∈ overlapCentersAtDepth Q j, ∫⁻ (x : Vec d), f x ∂normalizedOverlapCubeMeasure S ≤ 3 ^ d * ∫⁻ (x : Vec d), f x ∂normalizedCubeMeasure Q

Normalized finite-overlap comparison. Averaging the normalized overlap cube integrals over the retained centers costs only the pointwise overlap multiplicity 3^d relative to the normalized parent cube integral.