StepSevenCaccGradient

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

t.regularity Step 7c: e.gradient.with.shom

The target

  ν^{1/2}‖∇u‖_{L²((z+□_{n+1}) ∩ □_m)}
    ≤ C σ_{n'}^{1/2} 3^{(3/4)(1-α)(m-n)} 3^{-(m'-1)}
        ‖u - (u)_{(z+□_{m'-1})∩□_m}‖_{L²((z+□_{m'-1})∩□_m)}
      + C 3^{(3/4)(1-α)(m-n)} 3^{m/2} ( σ_m^{-1/2}[𝐠]_{W^{1/2,∞}(□_m)}
          + σ_m^{1/2}‖∇h‖_{W^{1/2,∞}(□_m)} 1_{z ∉ □_{m-1}} ) ,

C = C(d, c_*), and 3/4 = 1/4 (volume) + 1/2 (Hölder).

The scalar carriers

Following's StepSixHolderExponent, the step is proved on the S the display names, so that the composition is a theorem about the two exponents and nothing else:

• gradLoc — ν^{1/2}‖∇u‖_{L²((z+□_{n+1})∩□_m)}: for 𝐚_L = ν I + 𝐤 with 𝐤 antisymmetric this is the symmetric coefficient energy, so the reading is literally the manuscript's quantity.
• gradCore — the same energy on the Caccioppoli core U_{n'-2}.
• volFac — 3^{(d/2)(n'-n)}, discharged here against the Step-3 budget and the C₁ floor.
• lamLo — Λ_{1/4,2}(z + □_{n'}; 𝐚_{L,n'}), the Caccioppoli's ellipticity coefficient.
• shomNp — σ_{n'}.
• oscLo — 3^{-n'}‖u - (u)_{U_{n'}}‖_{L²(U_{n'})}.
• oscHi — 3^{-(m'-1)}‖u - (u)_{U_{m'-1}}‖_{L²(U_{m'-1})}.
• dataOsc — Step 6's OWN data leg, 3^{m/2}(σ_m^{-1}[𝐠]_{W^{1/2,∞}(□_m)} + ‖∇h‖_{W^{1/2,∞}(□_m)}1_{z∉□_{m-1}}).
• dataM — the Caccioppoli's own data leg at scale n', after e.lambda.stability.applied.

The three conditional inputs, and nothing else

The display-named theorems carry exactly three conditional inputs:

• hcacc — l.coarse.grained.Caccioppoli.RHS applied at the good scale n', in square-root (energy-norm) form. See that module.
• hlambda — e.lambda.stability.applied, the upper leg at k' = n': Λ_{1/4,2}(z+□_{n'};𝐚_{L,n'})1_{G} ≤ C σ_{n'}.
• hosc — e.oscillation.Holder.bound at scale n', in exactly the shape oscillationHolderBound_of_iterationResult produces.

Everything else is discharged: the volume factor's budget arithmetic (StepSevenCaccVolume), the exponent addition 1/4 + 1/2 = 3/4, and the R₂ ≥ 1 monotonicity that lets the Caccioppoli's own data leg ride the same power of three.

References

• ABK26, e.gradient.with.shom.
• ABK26, e.oscillation.Holder.bound; e.lambda.stability.applied.

1. The composition core

theorem Algsuperdiff.Section4.Provider.Regularity.gradientWithShom_compose {Cvol Ccacc Cosc Clam R1 R2 gradLoc gradCore volFac oscLo oscHi dataOsc dataM lamLo shomNp : ℝ} (hCvol : 0 ≤ Cvol) (hCcacc : 0 ≤ Ccacc) (hCosc : 0 ≤ Cosc) (hClam : 0 ≤ Clam) (hR1 : 0 ≤ R1) (hR2one : 1 ≤ R2) (hgradCore : 0 ≤ gradCore) (hoscLo : 0 ≤ oscLo) (hoscHi : 0 ≤ oscHi) (hdataOsc : 0 ≤ dataOsc) (hdataM : 0 ≤ dataM) (hvol : gradLoc ≤ volFac * gradCore) (hvolB : volFac ≤ Cvol * R1) (hcacc : gradCore ≤ Ccacc * (√lamLo * oscLo) + Ccacc * dataM) (hlambda : lamLo ≤ Clam * shomNp) (hosc : oscLo ≤ Cosc * R2 * oscHi + Cosc * R2 * dataOsc) : gradLoc ≤ Cvol * Ccacc * (Cosc * √Clam + 1) * √shomNp * (R1 * R2) * oscHi + Cvol * Ccacc * (Cosc * √Clam + 1) * (R1 * R2) * (√shomNp * dataOsc + dataM)

The Step-7c composition, on abstract reals.

From the four ingredients

  gradLoc  ≤ volFac · gradCore                 (the volume half)
  volFac   ≤ Cvol · R₁                         (the budget, StepSevenCaccVolume)
  gradCore ≤ Ccacc·(√lamLo · oscLo) + Ccacc·dataM        (hcacc)
  lamLo    ≤ Clam · shomNp                                (hlambda)
  oscLo    ≤ Cosc·R₂·oscHi + Cosc·R₂·dataOsc              (hosc)

together with 1 ≤ R₂, the display follows at the single output constant Cvol · Ccacc · (Cosc·√Clam + 1) and the single power R₁·R₂. Every step is a product of nonnegative reals; no transcendental atom occurs.

2. e.gradient.with.shom

theorem Algsuperdiff.Section4.Provider.Regularity.one_le_rpow_three_stepSixExponent {c alpha : ℝ} {n m : ℤ} (hc : 0 ≤ c) (halpha : alpha ≤ 1) (hnm : n ≤ m) : 1 ≤ Real.rpow 3 (c * stepSixExponent alpha n m)

1 ≤ 3^{c·(1-α)(m-n)} for c ≥ 0 in the Step-1/Step-3 regime.

theorem Algsuperdiff.Section4.Provider.Regularity.rpow_three_stepSixExponent_mul {c1 c2 alpha : ℝ} {n m : ℤ} : Real.rpow 3 (c1 * stepSixExponent alpha n m) * Real.rpow 3 (c2 * stepSixExponent alpha n m) = Real.rpow 3 ((c1 + c2) * stepSixExponent alpha n m)

3^{c₁ t} · 3^{c₂ t} = 3^{(c₁+c₂) t} at the Step-6 exponent argument.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenGradientWithShom (d : ℕ) {C1 alpha delta : ℝ} {B : ℕ} {n m n' : ℤ} {Ccacc Cosc Clam gradLoc gradCore oscLo oscHi dataOsc dataM lamLo shomNp : ℝ} (hC1 : 2 * ↑d + 2 ≤ C1) (halpha0 : 0 ≤ alpha) (halpha1 : alpha ≤ 1) (hnm : n ≤ m) (hdelta : delta ≤ C1⁻¹ * (1 - alpha)) (hgap : n' - n ≤ ↑B + 6) (hbudget : ↑B ≤ delta * (↑(m - n).toNat + 1)) (hCcacc : 0 ≤ Ccacc) (hCosc : 0 ≤ Cosc) (hClam : 0 ≤ Clam) (hgradCore : 0 ≤ gradCore) (hoscLo : 0 ≤ oscLo) (hoscHi : 0 ≤ oscHi) (hdataOsc : 0 ≤ dataOsc) (hdataM : 0 ≤ dataM) (hvol : gradLoc ≤ Real.rpow 3 (↑d / 2 * (↑n' - ↑n)) * gradCore) (hcacc : gradCore ≤ Ccacc * (√lamLo * oscLo) + Ccacc * dataM) (hlambda : lamLo ≤ Clam * shomNp) (hosc : oscLo ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * oscHi + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * dataOsc) : gradLoc ≤ Real.rpow 3 (3 * ↑d + 1 / 4) * Ccacc * (Cosc * √Clam + 1) * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * oscHi + Real.rpow 3 (3 * ↑d + 1 / 4) * Ccacc * (Cosc * √Clam + 1) * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * dataOsc + dataM)

e.gradient.with.shom, as printed.

The Caccioppoli at the lowest good scale n', the Hölder bound at that same scale, and the volume factor, composed. The exponent is the printed `3/4 = 1/4

• 1/2`.

The data bracket is the honest σ_{n'}^{1/2}·dataOsc + dataM; see the module docstring for the (separately proved) collapse to the printed 3^{m/2}(σ_m^{-1/2}[𝐠] + σ_m^{1/2}‖∇h‖1).

hcacc, hlambda, hosc are the only conditional inputs.