Coarse-graining support: Support.Deterministic.WeakNormInterfacesComponentwise

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

theorem HCPolySupport.abs_cubeBesovPairing_le_note_constant_mul_of_uniform_bound_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 < B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 u * B

theorem HCPolySupport.abs_cubeBesovPairing_le_note_constant_mul_of_uniform_bound_two_two_of_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) {B : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hB : 0 ≤ B) (hnorm : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 2 N g ≤ B) (hmem : CubeBesovDualLocalMemLpGlobal Q 2 g) : |cubeBesovPairing Q u g| ≤ 3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 u * B

theorem HCPolySupport.absCubeAverage_dot_le_componentBounds_twoTwo_noMeanTerm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) (B : Fin d → ℝ) (hs : 0 < s) (hu : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hB : ∀ (i : Fin d), 0 ≤ B i) (hnorm : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q s 2 2 N fun (x : Vec d) => g x i) ≤ B i) (hmem : ∀ (i : Fin d), CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => g x i) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * cubeBesovCircNorm Q s 2 2 fun (x : Vec d) => u x i) * B i

theorem HCPolySupport.memLp_on_descendant_of_memLp_generic {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {Q R : TriadicCube d} {j : ℕ} {p : ENNReal} {f : Vec d → E} (hR : R ∈ descendantsAtDepth Q j) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp f p (normalizedCubeMeasure R)

theorem HCPolySupport.memLp_component_of_memLp {d : ℕ} {Q : TriadicCube d} (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.memLp_cubeFluctuationVec {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (cubeFluctuationVec Q u) 2 (normalizedCubeMeasure Q)

theorem HCPolySupport.cubeFluctuation_component_eq_cubeFluctuationVec_component {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) : (cubeFluctuation Q fun (x : Vec d) => u x i) = fun (x : Vec d) => cubeFluctuationVec Q u x i

theorem HCPolySupport.sqrt_sum_sq_const_mul_eq_componentwise {ι : Type u_1} (s : Finset ι) (c : ℝ) (F : ι → ℝ) (hc : 0 ≤ c) : √(∑ i ∈ s, (c * F i) ^ 2) = c * √(∑ i ∈ s, F i ^ 2)

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_le_partialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (N j : ℕ) (hj : j ∈ Finset.range (N + 1)) : cubeBesovNegativeVectorDepthSeminorm Q s u j ≤ cubeBesovNegativeVectorPartialSeminorm Q s N u

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_le_partialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (N j : ℕ) (hj : j ∈ Finset.range (N + 1)) : cubeBesovPositiveVectorDepthSeminorm Q s u j ≤ cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.cubeBesovCircDepthAverage_two_component_le_negativeVectorDepthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) (j : ℕ) : cubeBesovCircDepthAverage Q 2 (fun (x : Vec d) => u x i) j ≤ cubeBesovNegativeVectorDepthAverage Q u j

theorem HCPolySupport.besovCircDepth_component_le_negativeVectorDepth {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (j : ℕ) : cubeBesovCircDepthSeminorm Q s 2 (fun (x : Vec d) => u x i) j ≤ cubeBesovScaleWeight (-s) Q * cubeBesovNegativeVectorDepthSeminorm Q s u j

theorem HCPolySupport.besovCircPartial_twoOne_component_le_negativeVectorPartial {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) : (cubeBesovCircPartialNorm Q s 2 1 N fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-s) Q * cubeBesovNegativeVectorPartialSeminorm Q s N u

theorem HCPolySupport.besovCircPartial_twoTwo_component_le_negativeVectorPartial {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) : (cubeBesovCircPartialNorm Q s 2 2 N fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-s) Q * cubeBesovNegativeVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.circNorm_component_le_negativeVectorPartialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ B) : (cubeBesovCircNorm Q s 2 1 fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-s) Q * B

theorem HCPolySupport.norm_cubeAverage_smul_component_le_cutoffDualCoeff_mul_negativeVectorPartialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (φ : Vec d → ℝ) (i : Fin d) {Bφ B : ℝ} (hs : 0 < s) (hui : MeasureTheory.MemLp (fun (x : Vec d) => u x i) 2 (normalizedCubeMeasure Q)) (hBφ : 0 ≤ Bφ) (hφDual : ∀ (N : ℕ), cubeBesovDualTestNorm Q s 2 1 N φ ≤ Bφ) (hφMem : CubeBesovDualLocalMemLpGlobal Q 2 φ) (hPartial : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ B) : ‖cubeAverage Q fun (x : Vec d) => (φ x • u x) i‖ ≤ 3 ^ (↑d + s) * cubeBesovScaleWeight (-s) Q * Bφ * B

theorem HCPolySupport.sum_abs_apply_le_card_mul_norm {d : ℕ} (v : Vec d) : ∑ i : Fin d, |v i| ≤ ↑(Fintype.card (Fin d)) * ‖v‖

theorem HCPolySupport.sum_abs_mul_const_mul_le_card_mul_norm_mul_const_mul_of_nonneg {d : ℕ} (v : Vec d) {K W : ℝ} (hK : 0 ≤ K) (hW : 0 ≤ W) : ∑ i : Fin d, |v i| * (K * W) ≤ ↑(Fintype.card (Fin d)) * K * ‖v‖ * W

theorem HCPolySupport.circNorm_component_le_negativeVectorPartialBoundTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ B) : (cubeBesovCircNorm Q s 2 2 fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-s) Q * B

theorem HCPolySupport.cubeBesovCircNorm_two_one_component_le_scaleWeight_neg_mul_gap_geometric_of_bddAbove {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hgap : 0 < a - b) (u : Vec d → Vec d) (i : Fin d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q b N u)) : (cubeBesovCircNorm Q a 2 1 fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-a) Q * (√(1 - Real.rpow 3 (-2 * (a - b)))⁻¹ * cubeBesovNegativeVectorSeminormTwo Q b u)

Componentwise q = 1 circ control at a larger exponent from the full vector q = 2 negative seminorm at a smaller exponent, with the geometric loss from the exponent gap.

theorem HCPolySupport.circNorm_two_one_component_le_scaleGap_of_negativePartialBound {d : ℕ} (Q : TriadicCube d) {r t : ℝ} (ht : t ≤ r) (u : Vec d → Vec d) (i : Fin d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovScaleWeight (-t) Q * cubeBesovNegativeVectorPartialSeminorm Q t N u ≤ B) : (cubeBesovCircNorm Q r 2 1 fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight (-(r - t)) Q * B

Componentwise q = 1 circ control at a larger exponent from a scaled negative-vector partial bound at a smaller exponent.

theorem HCPolySupport.cubeLpNorm_two_component_le_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeLpNorm Q 2 fun (x : Vec d) => u x i) ≤ cubeLpNorm Q 2 u

theorem HCPolySupport.cubeBesovOscillation_two_component_le_cubeLpNorm_fluctuationVec {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovOscillation Q 2 fun (x : Vec d) => u x i) ≤ cubeLpNorm Q 2 (cubeFluctuationVec Q u)

theorem HCPolySupport.cubeBesovDepthAverage_two_component_le_positiveVectorDepthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) (j : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovDepthAverage Q 2 (fun (x : Vec d) => u x i) j ≤ cubeBesovPositiveVectorDepthAverage Q u j

theorem HCPolySupport.cubeBesovDepthWeight_eq_scaleWeight_mul_rpow {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovDepthWeight Q s j = cubeBesovScaleWeight s Q * Real.rpow 3 (s * ↑j)

theorem HCPolySupport.cubeBesovDepthSeminorm_two_component_le_scaleWeight_mul_positiveVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (j : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeBesovDepthSeminorm Q s 2 (fun (x : Vec d) => u x i) j ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorDepthSeminorm Q s u j

theorem HCPolySupport.besovPartial_component_le_positiveVectorPartial {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovPartialSeminorm Q s 2 2 N fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.topBesovPartial_component_le_positiveVectorPartial {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovPartialSeminormTop Q s 2 N fun (x : Vec d) => u x i) ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.cubeBesovDualLocalMemLpGlobal_component_of_memLp {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : CubeBesovDualLocalMemLpGlobal Q 2 fun (x : Vec d) => u x i

theorem HCPolySupport.cubeBesovDualLocalMemLpGlobal_of_memLp_two {d : ℕ} (Q : TriadicCube d) (g : Vec d → ℝ) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) : CubeBesovDualLocalMemLpGlobal Q 2 g

A scalar L² function is locally admissible as a p = 2 Besov dual test at every descendant scale.

theorem HCPolySupport.dualTestNorm_componentOneFluctuationVector_le_weightedBy_vectorPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => cubeFluctuationVec Q u x i) ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.dualTestNorm_componentTwoFluctuationVector_le_weightedBy_vectorPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (i : Fin d) (N : ℕ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeBesovDualTestNorm Q s 2 2 N fun (x : Vec d) => cubeFluctuationVec Q u x i) ≤ cubeBesovScaleWeight s Q * cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.abs_cubeAverage_vecDot_fluctuationVec_le_sum_note_terms_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_fluctuationVec_le_sum_sharp_note_terms_of_partialBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)| ≤ ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

Sharp fluctuation estimate without the redundant average tail on the negative Besov side. This is the bridge form of the sharp vectorized duality bound used in the note-facing Caccioppoli proof.

theorem HCPolySupport.abs_cubeAverage_vecDot_fluctuationVec_le_sum_sharp_note_terms_of_dualTestBounds {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminorm Q s N u ≤ Bu) (hdual : ∀ (i : Fin d) (N : ℕ), (cubeBesovDualTestNorm Q s 2 1 N fun (x : Vec d) => cubeFluctuationVec Q g x i) ≤ cubeBesovScaleWeight s Q * Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)| ≤ ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

Sharp fluctuation estimate with the positive-side input stated directly as componentwise dual-test bounds. This avoids forcing callers through the finite q = 2 positive Besov package when they already have an infinite-depth q = ∞ cutoff-product estimate.

theorem HCPolySupport.abs_cubeAverage_vecDot_fluctuationVec_le_sum_note_terms_of_partialBounds_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)| ≤ ∑ i : Fin d, (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) + cubeBesovScaleWeight s Q * ‖cubeAverage Q fun (x : Vec d) => u x i‖) * (cubeBesovScaleWeight s Q * Bg)

theorem HCPolySupport.abs_cubeAverage_vecDot_fluctuationVec_le_sum_sharp_note_terms_of_partialBounds_two_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → Vec d) {Bu Bg : ℝ} (hs : 0 < s) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hBg : 0 ≤ Bg) (hneg : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ Bu) (hpos : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N g ≤ Bg) : |cubeAverage Q fun (x : Vec d) => vecDot (u x) (cubeFluctuationVec Q g x)| ≤ ↑d * (3 ^ (↑d + s) * (cubeBesovScaleWeight (-s) Q * Bu) * (cubeBesovScaleWeight s Q * Bg))

Sharp q = 2 fluctuation estimate without the redundant average tail on the negative Besov side.