Coarse-graining support: Support.Deterministic.CoarseFluxResponse.RHSConstantEnvelope

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

Constant envelopes for the RHS coarse-flux response

The manuscript statement of §3.2.4 carries an unspecified dimensional constant C(d). The base coarseFluxResponseRHSBound names the displayed scalar RHS without this constant. This leaf module keeps the harmless constant envelope available at the split/recomposition and descendant-averaging surfaces.

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_fluxDefect_le_of_split_component_bounds {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV : Vec d → Vec d) {BdefectW BfluxV Ba0V B : ℝ} (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) ≤ BdefectW) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V) (hcomponents : √2 * (√2 * (BdefectW + BfluxV) + Ba0V) ≤ B) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ B

Generic target version of the §3.2.4 split-component recomposition theorem. This is useful when the component estimates close into C(d) times the named bare RHS rather than the bare RHS itself.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_const_mul_fluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (gradU gradW gradV g : Vec d → Vec d) {BdefectW BfluxV Ba0V : ℝ} (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) ≤ BdefectW) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V) (hcomponents : √2 * (√2 * (BdefectW + BfluxV) + Ba0V) ≤ C * coarseFluxResponseRHSBound Q a a0 s gradU g) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ C * coarseFluxResponseRHSBound Q a a0 s gradU g

Constant-envelope version of the one-cube §3.2.4 split recomposition.

theorem HCPolySupport.coarseFluxResponse_scaledSplitEnvelope_le_two_const_rhs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU g : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) : √2 * (√2 * (C * coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g + C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) + C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

The split-envelope triangle constants for component bounds that already carry the same nonnegative multiplier C.

theorem HCPolySupport.negativeBesovSeminormTwo_fluxDefect_le_two_mul_const_mul_fluxRHSBound_of_split {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU gradW gradV g : Vec d → Vec d) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (hgBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hgrad : ∀ x ∈ cubeSet Q, gradU x = gradW x + gradV x) (hdefectW_mem : MemVectorL2 (cubeSet Q) (fluxDefect a a0 gradW)) (hfluxV_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : MemVectorL2 (cubeSet Q) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectW_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N (fluxDefect a a0 gradW))) (hfluxV_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradW) ≤ C * coarseFluxResponseRHSHomogeneousSplitBound Q a a0 s gradU g) (hfluxV : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound Q a s g) (ha0V : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ C * coarseFluxResponseRHSPoincareCorrectionBound Q a a0 s g) : cubeBesovNegativeVectorSeminormTwo Q s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound Q a a0 s gradU g

Split-component recomposition when every component estimate closes into the same constant multiple of its compact §3.2.4 component.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_bound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (s : ℝ) (gradU gradW gradV : Vec d → Vec d) (j : ℕ) {BdefectW BfluxV Ba0V B : TriadicCube d → ℝ} (hgrad : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, gradU x = gradW x + gradV x) (hdefectW_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) (fluxDefect a a0 gradW)) (hfluxV_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectU_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hdefectW_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradW))) (hfluxV_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradW) ≤ BdefectW R) (hfluxV : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV R) (ha0V : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V R) (hcomponents : ∀ R ∈ descendantsAtDepth Q j, √2 * (√2 * (BdefectW R + BfluxV R) + Ba0V R) ≤ B R) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => B R ^ 2)

Descendant-localized split-component handoff to an arbitrary scalar envelope.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_const_mul_fluxRHSBound_of_split {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (gradU gradW gradV g : Vec d → Vec d) (j : ℕ) {BdefectW BfluxV Ba0V : TriadicCube d → ℝ} (hgrad : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, gradU x = gradW x + gradV x) (hdefectW_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) (fluxDefect a a0 gradW)) (hfluxV_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectU_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hdefectW_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradW))) (hfluxV_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradW) ≤ BdefectW R) (hfluxV : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ BfluxV R) (ha0V : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ Ba0V R) (hcomponents : ∀ R ∈ descendantsAtDepth Q j, √2 * (√2 * (BdefectW R + BfluxV R) + Ba0V R) ≤ C * coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => (C * coarseFluxResponseRHSBound R a a0 s gradU g) ^ 2)

Descendant-localized split-component handoff to C times the named bare one-cube RHS on every descendant.

theorem HCPolySupport.sqrt_descendantsAverage_const_mul_coarseFluxResponseRHSBound_sq_eq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU g : Vec d → Vec d) (j : ℕ) (hC_nonneg : 0 ≤ C) : √(descendantsAverage Q j fun (R : TriadicCube d) => (C * coarseFluxResponseRHSBound R a a0 s gradU g) ^ 2) = C * localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Pull a nonnegative scalar outside the descendant L² average of the named one-cube §3.2.4 RHS bound.

theorem HCPolySupport.negativeBesovFluxAverage_le_sqrt_descendantMean_const_mul_fluxRHSBound_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (C s : ℝ) (gradU g : Vec d → Vec d) (j : ℕ) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ C * coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => (C * coarseFluxResponseRHSBound R a a0 s gradU g) ^ 2)

Descendant-localized §3.2.4 handoff from pointwise one-cube bounds with a caller-supplied scalar envelope.

theorem HCPolySupport.negativeBesovFluxAverage_le_const_mul_CoarseFluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU g : Vec d → Vec d) (j : ℕ) (hC_nonneg : 0 ≤ C) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ C * coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ C * localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Named descendant-localized §3.2.4 handoff with the nonnegative scalar envelope pulled outside the localized RHS norm.

theorem HCPolySupport.negativeBesovFluxAverage_le_two_mul_const_mul_CoarseFluxRHSBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU g : Vec d → Vec d) (j : ℕ) (hC_nonneg : 0 ≤ C) (hdefect_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hbound : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradU) ≤ 2 * C * coarseFluxResponseRHSBound R a a0 s gradU g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ 2 * C * localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Descendant-localized handoff for one-cube apex estimates whose target already contains the formal split/recomposition constant 2 * C.

theorem HCPolySupport.negativeBesovFluxAverage_le_two_mul_const_mul_CoarseFluxRHSBound_of_component {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {C s : ℝ} (gradU gradW gradV g : Vec d → Vec d) (j : ℕ) (hC_nonneg : 0 ≤ C) (hs : 0 < s) (hgBdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) (hgrad : ∀ R ∈ descendantsAtDepth Q j, ∀ x ∈ cubeSet R, gradU x = gradW x + gradV x) (hdefectW_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) (fluxDefect a a0 gradW)) (hfluxV_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul (a x) (gradV x)) (ha0V_mem : ∀ R ∈ descendantsAtDepth Q j, MemVectorL2 (cubeSet R) fun (x : Vec d) => matVecMul a0 (gradV x)) (hdefectU_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradU))) (hdefectW_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N (fluxDefect a a0 gradW))) (hfluxV_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul (a x) (gradV x))) (ha0V_bdd : ∀ R ∈ descendantsAtDepth Q j, BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N fun (x : Vec d) => matVecMul a0 (gradV x))) (hdefectW : ∀ R ∈ descendantsAtDepth Q j, cubeBesovNegativeVectorSeminormTwo R s (fluxDefect a a0 gradW) ≤ C * coarseFluxResponseRHSHomogeneousSplitBound R a a0 s gradU g) (hfluxV : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (gradV x)) ≤ C * coarseFluxResponseRHSWeakFluxCorrectionBound R a s g) (ha0V : ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul a0 (gradV x)) ≤ C * coarseFluxResponseRHSPoincareCorrectionBound R a a0 s g) : localizedFluxDefectNegativeBesovAverageTwo Q s (fluxDefect a a0 gradU) j ≤ 2 * C * localizedCoarseFluxResponseRHSBound Q a a0 s j gradU g

Descendant-localized split-component handoff with the formal 2 * C split/recomposition constant already included in the localized endpoint.