Documentation

LeanPool.Superdiffusion.Support.HighContrast.Corridor.FixedPhase.Recombination

Recombination #

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The G-factorization of the fixed-phase observable #

For the Efron–Stein step of Proposition 4.3 (p.fixed.phase.variance) the fixed phase observable

F_Οƒ(a) = P Β· 𝐀(U; a_Οƒ) P, U := cubeSet (originCube d m), a_Οƒ := corridorField β„“ Οƒ a

must be exhibited as a measurable function of the independent core restrictions Y_k := a|_{coreBox β„“ Οƒ k} for the finitely many cores k meeting U. This file builds the reconstruction map corePatch from a tuple of per-core fields, and proves the exact factorization

F_Οƒ (corePatch K (fun k => a|_{coreBox k})) = F_Οƒ a.

The reconstruction has a clean closed form on the diagonal input: for R a k := restrictCoeffField (coreBox β„“ Οƒ k) a,

corePatch K (fun k => R a k) = extendByIdCoeffField (⋃ k ∈ K, coreBox β„“ Οƒ k) a,

an ambient-measurable self-map (measurable_extendByIdCoeffField). The coarse matrix only sees U, and on U the corridor of this glued field agrees with the corridor of a (corridors are 1; the residual U βˆ– corridor is covered by the cores in K), so the two coarse matrices coincide.

The cores are pairwise disjoint (disjoint_coreBox, from the 2-separation areUnitSeparated_coreBox), which makes the indicator-sum reconstruction well-defined.

Pairwise disjointness of the cores #

source
theorem HCPolySupport.disjoint_coreBox {d : β„•} {β„“ : ℝ} (hβ„“ : 0 ≀ β„“) (Οƒ : Vec d) {k k' : Fin d β†’ β„€} (hne : k β‰  k') :
Disjoint (coreBox β„“ Οƒ k) (coreBox β„“ Οƒ k')

Distinct cores are disjoint: they are 2-separated (areUnitSeparated_coreBox), so a common point would have self-distance β‰₯ 1 > 0.

source
theorem HCPolySupport.not_mem_coreBox_of_mem {d : β„•} {β„“ : ℝ} (hβ„“ : 0 ≀ β„“) (Οƒ : Vec d) {k k' : Fin d β†’ β„€} (hne : k' β‰  k) {x : Vec d} (hx : x ∈ coreBox β„“ Οƒ k) :
x βˆ‰ coreBox β„“ Οƒ k'

A point of a core is in no other core.

The finite index set of cores meeting U #

source
noncomputable def HCPolySupport.coreMeetsFinset {d : β„•} {β„“ : ℝ} (hβ„“ : 0 < β„“) (Οƒ : Vec d) {U : Set (Vec d)} (hU : Bornology.IsBounded U) :
Finset (Fin d β†’ β„€)

The finite set of core indices whose core meets the bounded region U.

Equations
Instances For
    source
    @[simp]
    theorem HCPolySupport.mem_coreMeetsFinset {d : β„•} {β„“ : ℝ} (hβ„“ : 0 < β„“) (Οƒ : Vec d) {U : Set (Vec d)} (hU : Bornology.IsBounded U) (k : Fin d β†’ β„€) :
    k ∈ coreMeetsFinset hβ„“ Οƒ hU ↔ (coreBox β„“ Οƒ k ∩ U).Nonempty

    The core-restriction reconstruction map #

    source
    noncomputable def HCPolySupport.corePatch {d : β„•} (β„“ : ℝ) (Οƒ : Vec d) (K : Finset (Fin d β†’ β„€)) (y : β†₯K β†’ CoeffField d) :
    CoeffField d

    Reconstruct an ambient coefficient field from a tuple of per-core fields y : β†₯K β†’ CoeffField d. On the (disjoint) core coreBox β„“ Οƒ k it reads y k; off every core it is the identity. The indicator-sum form is well-defined because the cores are pairwise disjoint (at most one summand is nonzero).

    Equations
    Instances For
      source
      theorem HCPolySupport.corePatch_apply_of_mem {d : β„•} {β„“ : ℝ} (hβ„“ : 0 ≀ β„“) (Οƒ : Vec d) {K : Finset (Fin d β†’ β„€)} (y : β†₯K β†’ CoeffField d) {kβ‚€ : Fin d β†’ β„€} (hkβ‚€ : kβ‚€ ∈ K) {x : Vec d} (hx : x ∈ coreBox β„“ Οƒ kβ‚€) :
      corePatch β„“ Οƒ K y x = y ⟨kβ‚€, hkβ‚€βŸ© x

      On the core coreBox β„“ Οƒ kβ‚€ (with kβ‚€ ∈ K) the reconstruction reads y ⟨kβ‚€βŸ©.

      source
      theorem HCPolySupport.corePatch_apply_of_not_mem {d : β„•} {β„“ : ℝ} (Οƒ : Vec d) {K : Finset (Fin d β†’ β„€)} (y : β†₯K β†’ CoeffField d) {x : Vec d} (hx : βˆ€ k ∈ K, x βˆ‰ coreBox β„“ Οƒ k) :
      corePatch β„“ Οƒ K y x = 1

      Off every core in K, the reconstruction is the identity.

      The closed form of the reconstruction on core restrictions #

      source
      def HCPolySupport.coreUnion {d : β„•} (β„“ : ℝ) (Οƒ : Vec d) (K : Finset (Fin d β†’ β„€)) :
      Set (Vec d)

      The union of the cores in K.

      Equations
      Instances For
        source
        theorem HCPolySupport.mem_coreUnion {d : β„•} {β„“ : ℝ} {Οƒ : Vec d} {K : Finset (Fin d β†’ β„€)} {x : Vec d} :
        x ∈ coreUnion β„“ Οƒ K ↔ βˆƒ k ∈ K, x ∈ coreBox β„“ Οƒ k
        source
        theorem HCPolySupport.corePatch_restrict_eq_extendById {d : β„•} {β„“ : ℝ} (hβ„“ : 0 ≀ β„“) (Οƒ : Vec d) (K : Finset (Fin d β†’ β„€)) (a : CoeffField d) :
        (corePatch β„“ Οƒ K fun (k : β†₯K) => restrictCoeffField (coreBox β„“ Οƒ ↑k) a) = extendByIdCoeffField (coreUnion β„“ Οƒ K) a

        Closed form. Feeding the core-restrictions of a single field a to the reconstruction yields the identity-extension of a off the union of the cores. This is the key identity: the reconstruction of a diagonal tuple is a genuine ambient-measurable self-map (extendByIdCoeffField).

        The extendByIdCoeffField self-map is measurable #

        source
        theorem HCPolySupport.measurable_extendByIdCoeffField {d : β„•} (W : Set (Vec d)) :
        Measurable (extendByIdCoeffField W)

        The identity-extension self-map is ambient-measurable, by the same pointwise/local case-split as measurable_corridorField: each entry is a by_cases x ∈ W between a coordinate evaluation and the constant 1, and the map is spatially local.

        The coarse matrix sees only U #

        source
        theorem HCPolySupport.coarseBlockMatrix_eq_of_eqOn {d : β„•} {U : Set (Vec d)} (hU : MeasurableSet U) {a b : CoeffField d} (hab : Set.EqOn a b U) :
        coarseBlockMatrix U a = coarseBlockMatrix U b

        If two fields agree pointwise on the measurable set U, their coarse block matrices on U coincide (both equal the coarse matrix of the common U-restriction).

        The exact factorization (Part 1c) #

        source
        theorem HCPolySupport.corridorField_extendById_eqOn {d : β„•} {β„“ : ℝ} (hβ„“ : 0 < β„“) (Οƒ : Vec d) {K : Finset (Fin d β†’ β„€)} {U : Set (Vec d)} (hK : βˆ€ (k : Fin d β†’ β„€), (coreBox β„“ Οƒ k ∩ U).Nonempty β†’ k ∈ K) (a : CoeffField d) :
        Set.EqOn (corridorField β„“ Οƒ (extendByIdCoeffField (coreUnion β„“ Οƒ K) a)) (corridorField β„“ Οƒ a) U

        On U, the corridor of the identity-extension extendByIdCoeffField W a (with W βŠ‡ U βˆ– corridorSet) agrees pointwise with the corridor of a: on the corridor both are 1; off the corridor inside U the point lies in some core of K, so the extension reads a.

        source
        theorem HCPolySupport.phaseObservable_corePatch_restrict_eq {d : β„•} {β„“ : ℝ} (hβ„“ : 0 < β„“) {m : β„€} {Οƒ : Vec d} (P : BlockVec d) {K : Finset (Fin d β†’ β„€)} (hK : βˆ€ (k : Fin d β†’ β„€), (coreBox β„“ Οƒ k ∩ cubeSet (originCube d m)).Nonempty β†’ k ∈ K) (a : CoeffField d) :
        blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField β„“ Οƒ (corePatch β„“ Οƒ K fun (k : β†₯K) => restrictCoeffField (coreBox β„“ Οƒ ↑k) a))) P) = blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) (corridorField β„“ Οƒ a)) P)

        Part 1c (exact G-factorization). With U := cubeSet (originCube d m) and K the core indices meeting U, reconstructing the fixed-phase observable from the per-core restrictions of a reproduces F_Οƒ(a) exactly.