RootClauseBFinalAssembly #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. Two missing monotonicity steps in the C_B slot #
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseBDataMConst_mono
(d : ℕ)
{CBc CBc' : ℝ}
(h : CBc ≤ CBc')
:
rootClauseBDataMConst is monotone in its C_Bc slot.
theorem
Algsuperdiff.Section4.Provider.Regularity.rootClauseBCaccUniform_mono
(C : ℝ)
{CB CB' : ℝ}
(hCB : 0 ≤ CB)
(h : CB ≤ CB')
:
rootClauseBCaccUniform is monotone in its C_B slot.
1b. The Hölder constants are nonnegative #
theorem
Algsuperdiff.Section4.Provider.Regularity.holderHalf_const_nonneg
{d : ℕ}
[NeZero d]
{m : ℤ}
{K : ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f)
:
0 ≤ K is not a hypothesis, it is a consequence.
The frozen root prints HolderSeminormBoundOn (□_m) (1/2) K f and no sign
condition on K; every §4.4 producer nevertheless binds 0 ≤ K. The binder
is redundant: the open cube contains 0 and the point (3^m/4)·𝟙, whose
distance is positive, so 0 ≤ ‖f y - f 0‖ ≤ K‖y‖^{1/2} forces 0 ≤ K.