ObservationScaleFiniteCover

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

Observation-scale finite-cover transport

This module transports the lower-clause two-term homogenization-error bound from the cutoff cube to a larger observation cube. The transport is carried out on the genuine measurable representative. Translation covariance is used only through the cutoff-sample action, and the spatial enlargement is paid for by descendant averages, finite maxima, and the geometric depth weights already present in the q = 2 error.

The declarations here are internal Provider estimates.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.twoTermSquareConst : ℝ

The common constant for squaring the two-term observation-scale tail estimate.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.twoTermSquareConst = 1 + 4 * (3 * max 1 (Real.log 2)) ^ (1 / 4)⁻¹

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.cutoffCellErrorSq {d : ℕ} (M : ABKModel d) (L : ℤ) (u : ℝ) (R : HCPolySupport.TriadicCube d) : Cutoff.CutoffSample d → ℝ

The measurable square of the cutoff-scale error at a translated scale-L cell. The coefficient and normalizer stay frozen at L.

Equations

• One or more equations did not get rendered due to their size.

Raw/representative finite cover

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.cutoffCellErrorRawSq {d : ℕ} (M : ABKModel d) (L : ℤ) (u : ℝ) (R : HCPolySupport.TriadicCube d) : Cutoff.CutoffSample d → ℝ

The squared homogenization error for one cutoff cell against the isotropic comparator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleErrorLayerRaw {d : ℕ} (M : ABKModel d) (L m : ℤ) (t : ℝ) (ell : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The geometrically weighted block-response error at one observation depth.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleFineTailRaw {d : ℕ} (M : ABKModel d) (L m : ℤ) (t : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The infinite error tail below the cutoff scale.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleCoarseParentAverage {d : ℕ} (M : ABKModel d) (L m : ℤ) (u : ℝ) (ell : ℕ) (omega : Cutoff.CutoffSample d) : ℝ

The largest parent-cube average of normalized cutoff-cell errors at one depth.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleCoarseEnvelope {d : ℕ} (M : ABKModel d) (L m : ℤ) (t u : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The finite weighted envelope of coarse parent-cube error averages.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleCellErrorSup {d : ℕ} (M : ABKModel d) (L m : ℤ) (u : ℝ) (omega : Cutoff.CutoffSample d) : ℝ

The maximum normalized cutoff-cell error at the cutoff scale.

Equations

• One or more equations did not get rendered due to their size.

Probabilistic aggregation over the finite cover

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationDepthScale (d ell : ℕ) : ℝ

The dimension- and depth-dependent stochastic scale for the observation error.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleFineDepthFactor (d r : ℕ) : ℝ

The geometric depth factor bounding the fine part of the observation error.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.observationScaleFiniteCoverConst (d : ℕ) : ℝ

The common constant for the observation-scale finite-cover estimate.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Homogenization.observationScaleFiniteCover_sq_isBigOWith_gammaQuarter (d : ℕ) : ∃ (Cobs : ℝ), 1 ≤ Cobs ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), (∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) → 1 / 16 ∈ Set.Icc (8 * M.gamma) 1 → ∀ L ≤ m - 1, HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (1 / 4)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffHomogenizationErrorRepresentative M L m (1 / 8) (Annealed.sigmaBar M L) omega ^ 2) (Cobs * ((↑E * (1 / 16)⁻¹ * √M.gamma) ^ 2 + ((1 / 16)⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹))) ^ 2))

Dimension-only finite-cover transport of the lower homogenization-error clause from the cutoff cube at 1/16 to the observation cube at 1/8.

The legal-window premise only specializes the displayed lower clause; the constant is chosen before the model, induction scale, and amplitude parameter. This is a Provider endpoint and carries no source-node status by itself.