StepSevenCaccFinalDisplay #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The two derived scalars, named #
noncomputable def
Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccConst
{d : ℕ}
(C : ℝ)
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch03.CoeffFamily d)
:
The Caccioppoli's output constant at the §4.4 pin, Ccacc = √P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccConst_nonneg
{d : ℕ}
(C : ℝ)
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch03.CoeffFamily d)
:
noncomputable def
Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccDataM
{d : ℕ}
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch03.CoeffFamily d)
(g : HCPolySupport.Vec d → HCPolySupport.Vec d)
:
The Caccioppoli's own data leg at the §4.4 pin, dataM.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccDataM_nonneg
{d : ℕ}
(Q : HCPolySupport.TriadicCube d)
(a : HCPolySupport.Book.Ch03.CoeffFamily d)
{g : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hg : HCPolySupport.Book.Ch03.ForceBesovRegularity Q stepOneS g)
:
2. e.gradient.with.shom with hvol and hcacc discharged #
theorem
Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenGradientWithShom_interior
(d : ℕ)
[NeZero d]
:
∃ (C : ℝ),
0 < C ∧ ∀ (M : Section3.ABKModel d) (L mf m n n' : ℤ) (Qf : HCPolySupport.TriadicCube d) {z : HCPolySupport.Vec d}
(omega : Section3.Cutoff.CutoffSample d)
(u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n')).carrier)
{g : HCPolySupport.Vec d → HCPolySupport.Vec d} {C1 alpha delta : ℝ} {B : ℕ} {Cosc Clam oscHi dataOsc shomNp : ℝ},
(∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun (y + z)) →
(∀ (y : HCPolySupport.Vec d), v.grad y = u.grad (y + z)) →
z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) →
n' ≤ m - 1 →
n + 1 ≤ n' - 2 →
HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf (Section3.Cutoff.translateCutoffSample z omega)) v g →
HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d n') stepOneS g →
2 * ↑d + 2 ≤ C1 →
0 ≤ alpha →
alpha ≤ 1 →
n ≤ m →
delta ≤ C1⁻¹ * (1 - alpha) →
n' - n ≤ ↑B + 6 →
↑B ≤ delta * (↑(m - n).toNat + 1) →
0 ≤ Cosc →
0 ≤ Clam →
0 ≤ oscHi →
0 ≤ dataOsc →
HCPolySupport.Book.Ch02.lambdaS (HCPolySupport.originCube d n') stepSevenCaccT
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega)) ≤ Clam * shomNp →
(3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow z m n')
fun (x : HCPolySupport.Vec d) =>
u.toFun x - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m n')
u.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * oscHi + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * dataOsc →
stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m (n + 1))
u.grad ≤ Real.rpow 3 (3 * ↑d + 1 / 4) * stepSevenCaccConst C (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega)) * (Cosc * √Clam + 1) * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * oscHi + Real.rpow 3 (3 * ↑d + 1 / 4) * stepSevenCaccConst C (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega)) * (Cosc * √Clam + 1) * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * dataOsc + stepSevenCaccDataM (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega))
g)
e.gradient.with.shom on the interior branch, with hvol and hcacc
discharged.
ν^{1/2}‖∇u‖_{L²(U_{n+1})}
≤ (3^{3d+1/4}·Ccacc·(Cosc√Clam+1)) · √σ · 3^{(3/4)(1-α)(m-n)} · oscHi
+ (3^{3d+1/4}·Ccacc·(Cosc√Clam+1)) · 3^{(3/4)(1-α)(m-n)}
· ( √σ · dataOsc + dataM ) ,
at the carriers of the module docstring. The surviving analytic inputs are
hlambda (row 2 of the derived-slot table, discharged in the _of_caps sibling
below) and hosc
(e.oscillation.Holder.bound).
theorem
Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenGradientWithShom_interior_of_caps
(d : ℕ)
[NeZero d]
:
∃ (C : ℝ),
0 < C ∧ ∀ (M : Section3.ABKModel d) (L mf m n n' : ℤ) (Qf : HCPolySupport.TriadicCube d) {z : HCPolySupport.Vec d}
(omega : Section3.Cutoff.CutoffSample d)
(u : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))
(v : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d n')).carrier)
{g : HCPolySupport.Vec d → HCPolySupport.Vec d} {C1 alpha delta : ℝ} {B : ℕ} {Cosc CB sigma oscHi dataOsc : ℝ},
(∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun (y + z)) →
(∀ (y : HCPolySupport.Vec d), v.grad y = u.grad (y + z)) →
z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) →
n' ≤ m - 1 →
n + 1 ≤ n' - 2 →
HCPolySupport.Book.Ch03.IsForcedEquation (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf (Section3.Cutoff.translateCutoffSample z omega)) v g →
HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d n') stepOneS g →
2 * ↑d + 2 ≤ C1 →
0 ≤ alpha →
alpha ≤ 1 →
n ≤ m →
delta ≤ C1⁻¹ * (1 - alpha) →
n' - n ≤ ↑B + 6 →
↑B ≤ delta * (↑(m - n).toNat + 1) →
0 ≤ Cosc →
0 ≤ CB →
0 ≤ oscHi →
0 ≤ dataOsc →
StepSevenLambdaCaps (HCPolySupport.originCube d (n' + 1))
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega))
sigma CB →
(3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow z m n')
fun (x : HCPolySupport.Vec d) =>
u.toFun x - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m n')
u.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * oscHi + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * dataOsc →
stepSevenNuGradNorm M.nu (ExcessDecay.truncatedWindow z m (n + 1))
u.grad ≤ Real.rpow 3 (3 * ↑d + 1 / 4) * stepSevenCaccConst C (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega)) * (Cosc * √(256 / 63 * CB) + 1) * √sigma * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * oscHi + Real.rpow 3 (3 * ↑d + 1 / 4) * stepSevenCaccConst C (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega)) * (Cosc * √(256 / 63 * CB) + 1) * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√sigma * dataOsc + stepSevenCaccDataM (HCPolySupport.originCube d n')
(Support.fluxCorrectedCoeffFamily M L mf Qf
(Section3.Cutoff.translateCutoffSample z omega))
g)
e.gradient.with.shom on the interior branch, with hvol, hcacc AND
hlambda discharged.
hlambda is row 2 of the derived-slot table
(StepSevenLambdaSlots.stepSevenLambdaS_lower_le_of_caps) at the parent cube
□_{n'+1}: from the clause-(B) record there, λ_{1/8,1}(□_{n'}) ≤ (256/63)··σ. The only surviving analytic input is hosc.