ObservationScaleFiniteCoverDepth

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

Internal deterministic depth transport for the observation-scale cover

This module contains only the deterministic multiscale inequalities used by ObservationScaleFiniteCover. It is separated to keep each Lean file focused and below the repository line limit.

Deterministic depth transport

noncomputable def Algsuperdiff.Section3.Provider.Homogenization.ObservationScaleFiniteCoverInternal.weightedDepthEnergySq (s : ℝ) (H : ℕ → ℝ) : ℝ

The sum of a depth-energy profile with the prescribed geometric weights.

Equations

• Algsuperdiff.Section3.Provider.Homogenization.ObservationScaleFiniteCoverInternal.weightedDepthEnergySq s H = ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s 2 n * H n

theorem Algsuperdiff.Section3.Provider.Homogenization.ObservationScaleFiniteCoverInternal.maxDescendantNormalizedBlockResponseAtDepth_le_error_sq {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {s : ℝ} (hs : 0 < s) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (N : ℕ) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q (Q.scale - ↑N) a a0 ≤ Real.rpow 3 (2 * s * ↑N) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a a0 ^ 2

A response at depth N is controlled by the squared lower-discount homogenization error on its root, with the exact q = 2 depth factor.

theorem Algsuperdiff.Section3.Provider.Homogenization.ObservationScaleFiniteCoverInternal.exists_mem_descendantsAtScale_split {d : ℕ} {Q S : HCPolySupport.TriadicCube d} {k l : ℤ} (hk : k ≤ Q.scale) (hl : l ≤ k) (hS : S ∈ HCPolySupport.descendantsAtScale Q l) : ∃ R ∈ HCPolySupport.descendantsAtScale Q k, S ∈ HCPolySupport.descendantsAtScale R l

theorem Algsuperdiff.Section3.Provider.Homogenization.ObservationScaleFiniteCoverInternal.normalizedBlockResponseMax_le_descendantsAverage {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (j : ℕ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q a a0 ≤ HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.Book.Ch02.normalizedBlockResponseMax R a a0

Subadditivity turns one normalized parent response into the average of the same normalized response over any fixed descendant generation.