GeneratorRenormalization

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

Generator renormalization — [ABK] Theorem B (t.homogenization)

At every scale m the coarse-grained generator is a constant multiple sigmaBar of the identity, quantitatively close to sqrt (nu^2 + cstar gamma^{-1} 3^{2 gamma m}), and the disorder solution u is compared with the homogenized solution v of the same Dirichlet problem: a single random error amplitude with Gaussian-type moments controls both the uniform difference u - v and the difference of the two Dirichlet energies.

Proved; reduces to the standard axioms.

theorem Algsuperdiff.Frozen.Section4.generator_renormalization (d : ℕ) (cstar : ℝ) (_hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (m : ℤ), ∃ (sigmaBarM : ℝ), 0 < sigmaBarM ∧ |sigmaBarM - √(M.nu ^ 2 + cstar * M.gamma⁻¹ * Real.rpow 3 (2 * M.gamma * ↑m))| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBarM ∧ ∃ (EB : Section3.Cutoff.CutoffSample d → ℝ), (∀ (omega : Section3.Cutoff.CutoffSample d), 0 ≤ EB omega) ∧ Measurable EB ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (EB omega) ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) ∧ ∀ᵐ (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) => sigmaBarM • 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 omega * (sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + (KhInf + Real.rpow 3 (↑m / 2) * Kh))) ∧ |(HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => M.nu * HCPolySupport.vecNormSq (u.grad y)) - HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v.grad y)| ≤ EB omega * (√sigmaBarM⁻¹ * Real.rpow 3 (↑m / 2) * Kg + √sigmaBarM * (KhInf + Real.rpow 3 (↑m / 2) * Kh)) ^ 2