RenormalizationFamilyCorrector

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

Renormalization families with the corrector clause

This module assembles the scale-indexed effective diffusivities and error variables supplied by generator renormalization while retaining the corrector estimate for the same witnesses.

theorem Algsuperdiff.Section5.Support.exists_renormalizationFamily_corrector (d : ℕ) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∃ (sigmaBar : ℤ → ℝ) (EB : ℤ → Section3.Cutoff.CutoffSample d → ℝ), (∀ (m : ℤ), 0 < sigmaBar m) ∧ (∀ (m : ℤ), |sigmaBar m - effectiveDiffusivity M.nu cstar M.gamma (3 ^ m)| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBar m) ∧ (∀ (m : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB m omega) ∧ (∀ (m : ℤ), Measurable (EB m)) ∧ (∀ (m : ℤ) (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB m omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ (m : ℤ), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (L : ℤ), m ≤ L → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (Kg Kh KhInf : ℝ), Section4.Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Section4.Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBar m • 1) (HCPolySupport.originCube d m) v h g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Section4.Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → Section4.Support.HasGradientOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) h.toFun h.grad → ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)), Real.rpow 3 (-↑m) * |u.toFun x - v.toFun x| ≤ EB m omega * ((sigmaBar m)⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))

The renormalization families over the scales, with the corrector clause retained for the same error family whose moments are controlled.