RestrictionBridge

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

Restriction measurability for continuous coefficient fields

LocalSigmaR is generated by spatial integrals, whereas CoarseGraining's structural-law interface uses RestrictionSigmaR, which also sees point values. There is no global comparison in this direction on RegCoeffField: two merely measurable fields can agree almost everywhere and disagree at one point.

This file proves the comparison after pullback along a samplewise continuous carrier map. A value at x is recovered as the limit of normalized smooth bumps centered at x. If x \in U, every such probe is supported in the strict epsilon-thickening of U; integral generators of the restricted field are handled directly by masking their probes with U.indicator.

The resulting containment is exact, hence stronger than the modulo-null containment in the completion of any source probability space. A locally uniform-limit corollary records the route used by cutoff fields. The final geometric lemmas make explicit the conversion from the ambient dist (the sup norm on Vec) to the manuscript's Euclidean vecNorm, retaining the strict slack supplied by open thickenings.

noncomputable def Algsuperdiff.Section3.Annealed.shrinkingBump {d : ℕ} (epsilon : ℝ) (hepsilon : 0 < epsilon) (n : ℕ) : ContDiffBump 0

Smooth bumps with outer radius tending to zero inside the prescribed spatial radius.

Equations

• Algsuperdiff.Section3.Annealed.shrinkingBump epsilon hepsilon n = { rIn := epsilon / (↑n + 1) / 2, rOut := epsilon / (↑n + 1), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def Algsuperdiff.Section3.Annealed.mollifierProbe {d : ℕ} (epsilon : ℝ) (hepsilon : 0 < epsilon) (n : ℕ) (x y : HCPolySupport.Vec d) : ℝ

Normalized translated bumps used to probe local coefficient averages.

Equations

• Algsuperdiff.Section3.Annealed.mollifierProbe epsilon hepsilon n x y = (Algsuperdiff.Section3.Annealed.shrinkingBump epsilon hepsilon n).normed MeasureTheory.volume (x - y)

theorem Algsuperdiff.Section3.Annealed.comap_restrictionSigmaR_le_comap_localSigmaR_thickening {d : ℕ} {Omega : Type u_1} (A : Omega → HCPolySupport.RegCoeffField d) (hA : ∀ (omega : Omega) (i j : Fin d), Continuous fun (x : HCPolySupport.Vec d) => (A omega).toFun x i j) (U : Set (HCPolySupport.Vec d)) (hU : MeasurableSet U) (epsilon : ℝ) (hepsilon : 0 < epsilon) : MeasurableSpace.comap A (HCPolySupport.RestrictionSigmaR U hU) ≤ MeasurableSpace.comap A (HCPolySupport.LocalSigmaR (Metric.thickening epsilon U))

Pulling CoarseGraining restriction information back along a samplewise continuous carrier map loses no information after enlarging the integral observation set by any positive amount.

This is deliberately a map-specific statement. The corresponding global comparison RestrictionSigma hU ≤ LocalSigmaR ... is false on the full carrier because RegCoeffField permits changes on null sets.

theorem Algsuperdiff.Section3.Annealed.indep_restrictionSigmaR_map_of_indep_localSigmaR_thickenings {d : ℕ} {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} (A : Omega → HCPolySupport.RegCoeffField d) (hAmeas : Measurable A) (hA : ∀ (omega : Omega) (i j : Fin d), Continuous fun (x : HCPolySupport.Vec d) => (A omega).toFun x i j) (U V : Set (HCPolySupport.Vec d)) (hU : MeasurableSet U) (hV : MeasurableSet V) (epsilon : ℝ) (hepsilon : 0 < epsilon) (hlocal : ProbabilityTheory.Indep (MeasurableSpace.comap A (HCPolySupport.LocalSigmaR (Metric.thickening epsilon U))) (MeasurableSpace.comap A (HCPolySupport.LocalSigmaR (Metric.thickening epsilon V))) mu) : ProbabilityTheory.Indep (HCPolySupport.RestrictionSigmaR U hU) (HCPolySupport.RestrictionSigmaR V hV) (MeasureTheory.Measure.map A mu)

Generic independence transport for a continuous coefficient realization. Independence is assumed only for the two pulled-back integral-local sigma fields on strict thickenings. The conclusion is restriction-sigma independence under the actual pushforward law.

This theorem does not assert that the map has the hypothesis for any particular range. A cutoff construction must separately prove its local dependence and discharge the Euclidean separation premise.

theorem Algsuperdiff.Section3.Annealed.rho_lt_vecNorm_sub_of_mem_thickenings {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hUV : HCPolySupport.AreUnitSeparated U V) {epsilon rho : ℝ} (hslack : rho + 2 * epsilon ≤ 1) {x y : HCPolySupport.Vec d} (hx : x ∈ Metric.thickening epsilon U) (hy : y ∈ Metric.thickening epsilon V) : rho < HCPolySupport.Book.Ch02.vecNorm (x - y)

Unit separation in CoarseGraining's ambient metric leaves a strict Euclidean gap between open thickenings. The inequality rho + 2 * epsilon ≤ 1 is the rescaling budget: the strictness comes from membership in thickening.

theorem Algsuperdiff.Section3.Annealed.one_sub_two_mul_lt_vecNorm_sub_of_mem_thickenings {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hUV : HCPolySupport.AreUnitSeparated U V) {epsilon : ℝ} {x y : HCPolySupport.Vec d} (hx : x ∈ Metric.thickening epsilon U) (hy : y ∈ Metric.thickening epsilon V) : 1 - 2 * epsilon < HCPolySupport.Book.Ch02.vecNorm (x - y)

A convenient specialization exposing the full strict slack left by two open epsilon-thickenings.

theorem Algsuperdiff.Section3.Annealed.lt_vecNorm_sub_of_mem_scaled_thickenings {d : ℕ} {r epsilon range : ℝ} (hrpos : 0 < r) {U V : Set (HCPolySupport.Vec d)} (hUV : HCPolySupport.AreUnitSeparated U V) (hslack : range < r * (1 - 2 * epsilon)) {x y : HCPolySupport.Vec d} (hx : x ∈ r • Metric.thickening epsilon U) (hy : y ∈ r • Metric.thickening epsilon V) : range < HCPolySupport.Book.Ch02.vecNorm (x - y)

Positive rescaling transports the strict gap between open thickenings. The scale, thickening radius and requested separation are arbitrary.