UnitCubeTransfer #

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

Localization transfer between the unit cube and its triadic descendants #

The Section 2.4 sensitivity proofs apply a one-cube estimate on every triadic descendant z + cube_n of the unit cube and then aggregate. Two transfers are needed.

Root transfer #

The frozen scalars unitCubeLambda and unitCubeBigLambda are characterized against every compatible CoarseGraining triadic family, so any inequality proved at the family level for one compatible pair of families transfers to them. That is unitCubeLambda_inv_le_of_family_bound and unitCubeBigLambda_le_of_family_bound below; they are proved from exists_compatibleTriadicCoeffFamily together with the frozen characterization theorems, never by unfolding a Classical.choose definition.

Descendant transfer #

The perturbation a ↦ a + t h commutes with passing to a descendant cube: the descendant representative of any family compatible with perturbCoeffOn U a h t is a.e. equal to perturbCoeffOn of the descendant representative of any family compatible with a, with h restricted to the descendant cube. This is coeffOn_descendant_aeeq_perturbCoeffOn below, and it is what lets the per-descendant one-cube estimates of the neighbouring modules be fed into the aggregation lemmas.

Every declaration is an internal helper for the Section 2.4 sensitivity providers.

Restricting an `L^∞` skew field to a subdomain #

source

def Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.restrictLInfSkewMatrixFieldOn {d : ℕ} {U V : HCPolySupport.Book.Ch02.Domain d} (hsub : V.carrier ⊆ U.carrier) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) :

Frozen.Section24.LInfSkewMatrixFieldOn V

An L^∞ skew-symmetric matrix field on a domain restricts to any subdomain. The underlying representative is unchanged; only the L^∞ and a.e. skewness data are transported along the inclusion of measures.

Equations

Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.restrictLInfSkewMatrixFieldOn hsub h = ⟨⟨↑↑h, ⋯⟩, ⋯⟩

Instances For

source

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.restrictLInfSkewMatrixFieldOn_apply {d : ℕ} {U V : HCPolySupport.Book.Ch02.Domain d} (hsub : V.carrier ⊆ U.carrier) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (x : HCPolySupport.Vec d) :

↑↑(restrictLInfSkewMatrixFieldOn hsub h) x = ↑↑h x

The perturbation commutes with restriction #

source

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.perturbCoeffOn_toCoeffField {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (h : Frozen.Section24.LInfSkewMatrixFieldOn U) (t : ℝ) (x : HCPolySupport.Vec d) :

(Frozen.Section24.perturbCoeffOn U a h t).toCoeffField x = a.toCoeffField x + t • ↑↑h x

source

theorem Algsuperdiff.Section24.Sensitivity.Provider.Multiscale.coeffOn_descendant_aeeq_perturbCoeffOn {d : ℕ} (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (t : ℝ) (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h t)) {R : HCPolySupport.TriadicCube d} {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) :

(G.coeffOn R).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (restrictLInfSkewMatrixFieldOn ⋯ h) t)

Descendant localization of the perturbation. If F is any CoarseGraining family compatible with a at the origin cube and G is any CoarseGraining family compatible with a + t h there, then on every triadic descendant R of the origin cube the representative of G is a.e. the t-perturbation of the representative of F by the restriction of h.