CoarseGrainingSeminormScaling

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Positive homogeneity of the q = 2 negative Besov seminorm

Nothing here imports that file, and nothing here claims the anchor or any source node.

Why this is needed

ABK26's coarse-graining display e.homogenization.L2.interior has the scalar comparator on the left:

  3^{-sn/2} σ_n ‖∇u − ∇v‖_{H_hat^{-s/2}(x+□_n)}  ≤  … ,

and CoarseGraining's homogenizationComparisonNegativeBesovLHS likewise measures the field a₀(∇u − ∇v) = σ₀ (∇u − ∇v), not the bare gradient defect. The negative-norm-to-L² leg, on the other hand, consumes the bare gradient of an H¹₀ function. Moving the scalar across is exactly the positive homogeneity proved here — an identity, with no constant and no side condition.

Every step is elementary and local to CoarseGraining's definition chain cubeAverageVec → vecNormSq → descendantsAverage → depth seminorm → partial seminorm → sSup; the last step uses Mathlib's Real.smul_iSup_of_nonneg, which is unconditional because Real.sSup of an unbounded set is 0.

References

• ABK26, e.homogenization.L2.interior.
• Homogenization/Deterministic/WeakNormInterfaces/Definitions.lean (the definition chain).

1. Averages

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeAverageVec_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.cubeAverageVec Q fun (x : HCPolySupport.Vec d) => c • F x) = c • HCPolySupport.cubeAverageVec Q F

Cube averages of vector fields are homogeneous.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.descendantsAverage_const_mul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (c : ℝ) (G : HCPolySupport.TriadicCube d → ℝ) : (HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => c * G R) = c * HCPolySupport.descendantsAverage Q j G

Descendant averages are linear in a scalar factor.

2. The depth pieces

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovNegativeVectorDepthAverage_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : HCPolySupport.cubeBesovNegativeVectorDepthAverage Q (fun (x : HCPolySupport.Vec d) => c • F x) j = c ^ 2 * HCPolySupport.cubeBesovNegativeVectorDepthAverage Q F j

The depth-j block average scales by c².

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovNegativeVectorDepthSeminorm_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) {c : ℝ} (hc : 0 ≤ c) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (j : ℕ) : HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s (fun (x : HCPolySupport.Vec d) => c • F x) j = c * HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s F j

The depth-j negative seminorm scales by c for c ≥ 0.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovNegativeVectorPartialSeminormTwo_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) {c : ℝ} (hc : 0 ≤ c) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) (N : ℕ) : (HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : HCPolySupport.Vec d) => c • F x) = c * HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N F

The finite-depth q = 2 negative seminorm scales by c for c ≥ 0.

3. The seminorm

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeBesovNegativeVectorSeminormTwo_smul {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) {c : ℝ} (hc : 0 ≤ c) (F : HCPolySupport.Vec d → HCPolySupport.Vec d) : (HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s fun (x : HCPolySupport.Vec d) => c • F x) = c * HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s F

Positive homogeneity of the q = 2 negative Besov seminorm.

  [c F]_{B^{-s}_{2,2}(Q)} = c [F]_{B^{-s}_{2,2}(Q)}      (c ≥ 0) .

No boundedness hypothesis is needed: Real.sSup of an unbounded set is 0, so Real.smul_iSup_of_nonneg is unconditional.