Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.EnergyBridge.QuantitativeCutoff.Basic

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

noncomputable def HCPolySupport.scalarCutoffGradientField {d : ℕ} (η : Vec d → ℝ) : Vec d → Vec d

The vector cutoff field used in coarse Caccioppoli, obtained by applying the scalar cutoff gradient to the coordinate basis vectors.

Equations

• HCPolySupport.scalarCutoffGradientField η x i = (fderiv ℝ η x) (HCPolySupport.basisVec i)

@[simp]

theorem HCPolySupport.scalarCutoffGradientField_apply {d : ℕ} (η : Vec d → ℝ) (x : Vec d) (i : Fin d) : scalarCutoffGradientField η x i = (fderiv ℝ η x) (basisVec i)

theorem HCPolySupport.support_scalarCutoffGradientField_subset_tsupport {d : ℕ} (η : Vec d → ℝ) : Function.support (scalarCutoffGradientField η) ⊆ tsupport η

theorem HCPolySupport.scalarCutoffGradientField_eq_zero_of_notMem_tsupport {d : ℕ} {η : Vec d → ℝ} {x : Vec d} (hx : x ∉ tsupport η) : scalarCutoffGradientField η x = 0

@[simp]

theorem HCPolySupport.norm_basisVec {d : ℕ} (i : Fin d) : ‖basisVec i‖ = 1

theorem HCPolySupport.norm_scalarCutoffGradientField_le_fderiv {d : ℕ} (η : Vec d → ℝ) (x : Vec d) : ‖scalarCutoffGradientField η x‖ ≤ ‖fderiv ℝ η x‖

theorem HCPolySupport.continuous_scalarCutoffGradientField {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) : Continuous (scalarCutoffGradientField η)

theorem HCPolySupport.contDiff_scalarCutoffGradientField_component {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (i : Fin d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => scalarCutoffGradientField η x i

theorem HCPolySupport.memLp_top_scalarCutoffGradientField_of_bound_on_cubeSet {d : ℕ} (Q : TriadicCube d) {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) {Xi : ℝ} (hgrad : ∀ z ∈ cubeSet Q, ‖fderiv ℝ η z‖ ≤ Xi) : MeasureTheory.MemLp (scalarCutoffGradientField η) ⊤ (normalizedCubeMeasure Q)

theorem HCPolySupport.cubeLpNorm_infty_scalarCutoffGradientField_le_of_bound_on_cubeSet {d : ℕ} (Q : TriadicCube d) {η : Vec d → ℝ} {Xi : ℝ} (hXi : 0 ≤ Xi) (hgrad : ∀ z ∈ cubeSet Q, ‖fderiv ℝ η z‖ ≤ Xi) : cubeLpNorm Q ⊤ (scalarCutoffGradientField η) ≤ Xi

theorem HCPolySupport.scaledClosedCubeSet_subset_openCubeSet_of_lt_one {d : ℕ} (Q : TriadicCube d) {ρ : ℝ} (hρ_nonneg : 0 ≤ ρ) (hρ_lt_one : ρ < 1) : scaledClosedCubeSet Q ρ ⊆ openCubeSet Q

theorem HCPolySupport.scaledOpenCubeSet_subset_scaledClosedCubeSet_of_coord_lt {d : ℕ} (Q : TriadicCube d) (ρ : ℝ) : scaledOpenCubeSet Q ρ ⊆ scaledClosedCubeSet Q ρ

theorem HCPolySupport.QuantitativeCubeCutoff.tsupport_subset_scaledClosedCubeSet {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) : tsupport η.toFun ⊆ scaledClosedCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeCubeCutoff.support_scalarCutoffGradientField_subset_scaledClosedCubeSet {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) : Function.support (scalarCutoffGradientField η.toFun) ⊆ scaledClosedCubeSet Q ρ₂

theorem HCPolySupport.QuantitativeCubeCutoff.scalarCutoffGradientField_eq_zero_of_notMem_scaledClosedCubeSet {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) {x : Vec d} (hx : x ∉ scaledClosedCubeSet Q ρ₂) : scalarCutoffGradientField η.toFun x = 0

theorem HCPolySupport.cubeSet_subset_scaledClosedCubeSet_of_intersects_scaledClosedCubeSet_of_scaleFactor_le_gap {d : ℕ} {Q R : TriadicCube d} {ρinner ρouter : ℝ} (hgap : cubeScaleFactor R ≤ (ρouter - ρinner) * cubeRadius Q) (hinter : ∃ y ∈ cubeSet R, y ∈ scaledClosedCubeSet Q ρinner) : cubeSet R ⊆ scaledClosedCubeSet Q ρouter

A descendant cube that touches a smaller scaled cube is contained in a larger scaled cube, provided its side length fits in the radial buffer.

theorem HCPolySupport.cubeScaleFactor_le_gap_mul_cubeRadius_of_mem_descendantsAtDepth_of_triadicGapScaleChoice {d : ℕ} {Q R : TriadicCube d} {j k : ℕ} {ρinner ρouter : ℝ} (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρinner ρouter) (hkj : k ≤ j) : cubeScaleFactor R ≤ (ρouter - ρinner) * cubeRadius Q

The note's triadic gap scale makes depth-j descendants fit inside the radial buffer, as soon as j dominates the chosen scale.

theorem HCPolySupport.cubeScaleFactor_le_buffer_of_mem_descendantsAtDepth_of_triadicGapScaleChoice {d : ℕ} {Q R : TriadicCube d} {j k : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hkj : k ≤ j) : cubeScaleFactor R ≤ (ρ₂ - coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) * cubeRadius Q

The midpoint cutoff leaves a half-gap buffer, and the note's triadic scale still makes depth-j descendants fit inside that buffer.

theorem HCPolySupport.cubeScaleFactor_le_local_buffer_of_mem_descendantsAtDepth_succ_of_triadicGapScaleChoice {d : ℕ} {Q R : TriadicCube d} {j k : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hkj : k ≤ j) : cubeScaleFactor R ≤ (ρ₂ - coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) * (cubeRadius Q / 3)

One extra descendant generation fits the midpoint buffer at the Q.scale - 1 local-patch scale.

theorem HCPolySupport.QuantitativeCubeCutoff.tsupport_subset_openCubeSet_of_lt_one {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hρ₂_nonneg : 0 ≤ ρ₂) (hρ₂_lt_one : ρ₂ < 1) : tsupport η.toFun ⊆ openCubeSet Q

theorem HCPolySupport.QuantitativeCubeCutoff.support_scalarCutoffGradientField_subset_openCubeSet_of_lt_one {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hρ₂_nonneg : 0 ≤ ρ₂) (hρ₂_lt_one : ρ₂ < 1) : Function.support (scalarCutoffGradientField η.toFun) ⊆ openCubeSet Q

theorem HCPolySupport.QuantitativeCubeCutoff.scalarCutoffGradientField_eq_zero_of_notMem_openCubeSet_of_lt_one {d : ℕ} {Q : TriadicCube d} {ρ₁ ρ₂ : ℝ} (η : QuantitativeCubeCutoff Q ρ₁ ρ₂) (hρ₂_nonneg : 0 ≤ ρ₂) (hρ₂_lt_one : ρ₂ < 1) {x : Vec d} (hx : x ∉ openCubeSet Q) : scalarCutoffGradientField η.toFun x = 0

theorem HCPolySupport.quantitativeCubeCutoff_canonicalFun_tsupport_subset_openCubeSet {d : ℕ} (Q : TriadicCube d) {ρ₁ ρ₂ : ℝ} (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hρ₂_lt_one : ρ₂ < 1) : tsupport (QuantitativeCubeCutoff.canonicalFun Q ρ₁ ρ₂) ⊆ openCubeSet Q

noncomputable def HCPolySupport.quantitativeCubeCutoffCanonicalH10 {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) (hρ₁ : 0 < ρ₁) (hρ₁₂ : ρ₁ < ρ₂) (hρ₂_lt_one : ρ₂ < 1) : H10Function (openCubeSet Q)

Canonical cube cutoff packaged as an H10 test function on openCubeSet Q whenever the outer cutoff radius stays strictly inside the cube.

Equations

• HCPolySupport.quantitativeCubeCutoffCanonicalH10 Q ρ₁ ρ₂ hρ₁ hρ₁₂ hρ₂_lt_one = HCPolySupport.H10Function.ofContDiff ⋯ ⋯ ⋯ ⋯

theorem HCPolySupport.cubeAverage_quantitativeCubeCutoff_canonicalFun_pos {d : ℕ} (Q : TriadicCube d) : 0 < cubeAverage Q (QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4))

theorem HCPolySupport.half_pow_card_le_cubeAverage_quantitativeCubeCutoff_canonicalFun {d : ℕ} (Q : TriadicCube d) : (1 / 2) ^ d ≤ cubeAverage Q (QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4))

The canonical cutoff has a dimension-only lower average: it is identically one on the concentric half cube.

theorem HCPolySupport.inv_cubeAverage_quantitativeCubeCutoff_canonicalFun_le_two_pow_card {d : ℕ} (Q : TriadicCube d) : (cubeAverage Q (QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4)))⁻¹ ≤ 2 ^ d

The inverse average of the canonical cutoff is bounded by a dimension-only constant.

theorem HCPolySupport.cubeAverage_normalized_quantitativeCubeCutoff_canonicalFun_eq_one {d : ℕ} (Q : TriadicCube d) : (cubeAverage Q fun (x : Vec d) => (cubeAverage Q (QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4)))⁻¹ * QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4) x) = 1

theorem HCPolySupport.normalized_quantitativeCubeCutoff_canonicalFun_basic_controls {d : ℕ} (Q : TriadicCube d) : have η := QuantitativeCubeCutoff.canonicalFun Q (1 / 2) (3 / 4); have φ := fun (x : Vec d) => (cubeAverage Q η)⁻¹ * η x; cubeAverage Q φ = 1 ∧ MeasureTheory.AEStronglyMeasurable φ (volumeMeasureOn (cubeSet Q)) ∧ (∀ᵐ (x : Vec d) ∂volumeMeasureOn (cubeSet Q), ‖φ x‖ ≤ (cubeAverage Q η)⁻¹) ∧ ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ openCubeSet Q