RunningDiffusivityBridge

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

construction of the infinite-volume annealed diffusivity

CoarseGraining defines barSigmaLimit as the infimum of the scalarized annealed upper coefficients. Its Section 5.7 public positivity and primal/dual identification lemmas are stated under the stronger GammaSigmaCoarseGrainedEllipticity input. This file records that non-circular route for the Section 3 cutoff law.

The last theorem transports the resulting limit back across the triadic normalization used to obtain CoarseGraining's unit-range structural law. The conclusion is stated for the honest full matrices, since the auxiliary BlockMat record does not carry a topology.

theorem Algsuperdiff.Section3.Annealed.barSigmaAtScale_tendsto_barSigmaLimit_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : Filter.Tendsto (fun (n : ℕ) => hP.barSigmaAtScale hStruct ↑n) Filter.atTop (nhds (HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct))

Under (P4), the scalarized upper annealed coefficients converge to CoarseGraining's barSigmaLimit.

theorem Algsuperdiff.Section3.Annealed.barSigmaStarAtScale_tendsto_barSigmaStarLimit_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : Filter.Tendsto (fun (n : ℕ) => hP.barSigmaStarAtScale hStruct ↑n) Filter.atTop (nhds (HCPolySupport.Book.Ch05.Section57.barSigmaStarLimit hP hStruct))

Under (P4), the scalarized starred annealed coefficients converge to CoarseGraining's barSigmaStarLimit.

theorem Algsuperdiff.Section3.Annealed.barSigmaLimit_pos_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : 0 < HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct

(P4) already makes CoarseGraining's limiting upper scalar strictly positive.

theorem Algsuperdiff.Section3.Annealed.barSigmaLimit_eq_barSigmaStarLimit_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct = HCPolySupport.Book.Ch05.Section57.barSigmaStarLimit hP hStruct

Under (P4), the upper and starred annealed scalar limits coincide.

theorem Algsuperdiff.Section3.Annealed.barSigmaStarAtScale_tendsto_barSigmaLimit_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : Filter.Tendsto (fun (n : ℕ) => hP.barSigmaStarAtScale hStruct ↑n) Filter.atTop (nhds (HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct))

Under (P4), the starred scalar coefficients converge to the same positive scalar as the upper coefficients.

theorem Algsuperdiff.Section3.Annealed.annealedFullBlockMatrixAtScale_tendsto_barSigmaLimit_of_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw P) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct • 1) ((HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct)⁻¹ • 1))))

Under (P4), the honest full annealed block matrices converge entrywise to the block diagonal with the single positive scalar barSigmaLimit and its inverse.

theorem Algsuperdiff.Section3.Annealed.annealedFullBlockMatrixAtScale_tendsto_of_scaleNormalized_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (k : ℕ) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k P)) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k P)) : Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (HCPolySupport.Book.Ch05.Section57.barSigmaLimit ⋯ hStruct • 1) ((HCPolySupport.Book.Ch05.Section57.barSigmaLimit ⋯ hStruct)⁻¹ • 1))))

Spatial normalization does not alter the infinite-volume coefficient.

If a triadically normalized pushforward of P satisfies CoarseGraining's structural law and (P4), then the unnormalized annealed matrices converge to the same block diagonal. This is the bridge needed when the original cutoff has range sqrt d * 3^m rather than CoarseGraining's normalized unit range.

theorem Algsuperdiff.Section3.Annealed.scalar_eq_of_annealedFullBlockMatrixAtScale_tendsto {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} {σ τ : ℝ} (hσ : Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (σ • 1) (σ⁻¹ • 1))))) (hτ : Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (τ • 1) (τ⁻¹ • 1))))) : σ = τ

The positive scalar in an infinite-volume block-diagonal limit is unique.

theorem Algsuperdiff.Section3.Annealed.existsUnique_pos_annealedFullBlockMatrixAtScale_limit_of_scaleNormalized_P4 {d : ℕ} [NeZero d] {P : HCPolySupport.Book.Ch04.RestrictionCoeffLaw d} (hP : HCPolySupport.Book.Ch04.RestrictionLawCarrier P) (k : ℕ) (hStruct : HCPolySupport.Book.Ch04.RestrictionStructuralLaw (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k P)) (hP4 : HCPolySupport.Book.Ch05.QuantitativeCoarseGrainedEllipticity (HCPolySupport.Book.Ch04.restrictionScaleNormalizedLaw k P)) : ∃! σ : ℝ, 0 < σ ∧ Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale P ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch02.blockDiag (σ • 1) (σ⁻¹ • 1))))

A normalized structural law with (P4) gives existence and uniqueness of the positive scalar describing the unnormalized infinite-volume annealed block limit.