Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Provider.Homogenization.HomSeamSupClauseProvider

HomSeamSupClauseProvider #

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

THE BUDGETED CONDITIONAL PROVIDER AT THE SUP-FORM CLAUSE #

The deliverable #

  generator_renormalization_provider_of_supBundleBudget
      -- {0 < cstar, 0 < gamma0, 0 < Cgap} + {the bundle at the SUP shape}

The clause input is now the paper's own sup-over-depths multiscale clause (HomSpineSupFormClause.CoarseGrainingSupMultiscale), i.e. exactly the object HomSpineSupFormClause produces from the single-depth grid/smooth-dual comparison. The factor D3 is discharged here as at the budgeted geometric provider; the geometric factor rides inside C_en⁰(M) and is paid for by the frozen display's extra |log γ|.

The re-cut only forgets: the ℓ^p clause supply still drives this provider.

1. The spine endpoint at the sup-form bundle #

source
theorem Algsuperdiff.Section4.Provider.Homogenization.homogenization_spine_close_of_supBundleBudget (d : ℕ) [NeZero d] (hd : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) {Cst Cgap Cabs Ctop : ℝ} {KabsF : Section3.ABKModel d → ℝ} (hCst : 1 ≤ Cst) (hCgap : 0 ≤ Cgap) (hCabs : 0 ≤ Cabs) (hKabs : ∀ (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → 0 ≤ KabsF M) (hKbud : ∀ (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → KabsF M ≤ Cabs * |Real.log M.gamma|) (hCtop : 0 ≤ Ctop) :
∃ (gamma0 : ℝ) (C : ℝ), 0 < gamma0 ∧ 0 < C ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (X : Section3.Cutoff.CutoffSample d → ℕ∞), Measurable X → (∀ (N : ℕ), ↑(Section3.Cutoff.cutoffSampleLaw M) {omega : Section3.Cutoff.CutoffSample d | ↑N ≤ X omega} ≤ ENNReal.ofReal (Cst * Real.exp (-((1 - homAlpha M) ^ 2 * (↑N - Cst)) / (Cst * M.gamma)))) → ∀ (hs : 0 < homS M) (m : ℤ), (∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), SpineDatumCoarseGrainingRecutFluxHalfSupGrad M Cgap (seamEnlargedY M m Ctop (homMinimalScaleFactor (1 - homAlpha M) X)) m (homSeamBase M hs) ↑(Section3.Annealed.sigmaBar M m) ⋯ (KabsF M) omega) → ∃ (sigmaBar : ℝ), 0 < sigmaBar ∧ |sigmaBar - √(M.nu ^ 2 + cstar * M.gamma⁻¹ * Real.rpow 3 (2 * M.gamma * ↑m))| ≤ C * √M.gamma * |Real.log M.gamma| * sigmaBar ∧ ∃ (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 : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBar • 1) (HCPolySupport.originCube d m) v h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → 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 * (sigmaBar⁻¹ * 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) => sigmaBar * HCPolySupport.vecNormSq (v.grad y)| ≤ EB omega * (√sigmaBar⁻¹ * Real.rpow 3 (↑m / 2) * Kg + √sigmaBar * (KhInf + Real.rpow 3 (↑m / 2) * Kh)) ^ 2

The budgeted gradient spine closure at the sup-form datum.

2. The provider at the sup-form bundle #

source
theorem Algsuperdiff.Section4.Provider.Homogenization.generator_renormalization_provider_of_supBundleBudget (d : ℕ) [NeZero d] (hd : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) {gamma0res Cgap Ctop : ℝ} {CabsF : ℝ → ℝ} {KabsF : ℝ → Section3.ABKModel d → ℝ} (hg0res : 0 < gamma0res) (hCgap : 0 ≤ Cgap) (hCabs : ∀ (Creg : ℝ), 0 < Creg → 0 ≤ CabsF Creg) (hKabs : ∀ (Creg : ℝ), 0 < Creg → ∀ (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → 0 ≤ KabsF Creg M) (hKbud : ∀ (Creg : ℝ), 0 < Creg → ∀ (M : Section3.ABKModel d), 4 ≤ |Real.log M.gamma| → KabsF Creg M ≤ CabsF Creg * |Real.log M.gamma|) (hCtop : 0 ≤ Ctop) (hcore : ∀ (Creg : ℝ), 0 < Creg → SeamBundleOfRegularityHalfSupGradBudget d cstar gamma0res Cgap (KabsF Creg) Ctop Creg) :
∃ (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 : ℝ), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) (HCPolySupport.originCube d m) v h g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kg g → Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Kh h.grad → (∀ x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m), ‖h.grad x‖ ≤ KhInf) → 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

The budgeted gradient provider at the sup-form bundle.