WholeSpaceDenseRange

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

Dense range of the stream-field whole-space resolvent

At large shift, the normalized analytic minimal resolvent is an approximate identity on compactly supported continuous data. Near the support this uses uniform continuity and a fixed ball on which radius amplification is inactive. Far from the support, the amplified radius remains disjoint from the datum and the same shift-uniform envelope controls the resolvent. Contractivity and the density of compactly supported data give strong normalization on all of C₀, and hence dense range.

theorem Algsuperdiff.Section5.Field.abs_le_norm_dense {d : ℕ} (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : |f x| ≤ ‖f‖

theorem Algsuperdiff.Section5.Field.measurable_complBall {d : ℕ} (x : HCPolySupport.Vec d) (r : ℝ) : Measurable fun (y : HCPolySupport.Vec d) => (Metric.ball x r)ᶜ.indicator (fun (x : HCPolySupport.Vec d) => 1) y

theorem Algsuperdiff.Section5.Field.abs_complBall_le_one {d : ℕ} (x : HCPolySupport.Vec d) (r : ℝ) (y : HCPolySupport.Vec d) : |(Metric.ball x r)ᶜ.indicator (fun (x : HCPolySupport.Vec d) => 1) y| ≤ 1

theorem Algsuperdiff.Section5.Field.mul_toReal_streamAnalyticMinimalResolvent_compl_amp_le_envelope {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (hcut : streamUniformExhaustionCutoff M omega ↑mu < √↑mu * r) : ↑mu * ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu ((Metric.ball x (streamExhaustionAmp x r))ᶜ.indicator fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x).toReal ≤ streamUniformExhaustionEnvelope M omega (√↑mu * r)

The analytic tail outside the amplified ball is bounded by the common envelope whenever the base scale is beyond the logarithmic cutoff.

theorem Algsuperdiff.Section5.Field.mul_toReal_streamAnalyticMinimalResolvent_complBall_le_envelope {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (hmu : 1 ≤ ↑mu) (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) (hamp : streamExhaustionAmp x r = r) (hcut : streamUniformExhaustionCutoff M omega ↑mu < √↑mu * r) : ↑mu * ((streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu ((Metric.ball x r)ᶜ.indicator fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x).toReal ≤ streamUniformExhaustionEnvelope M omega (√↑mu * r)

If amplification is inactive, the preceding estimate is the ordinary complement-of-ball tail bound.

theorem Algsuperdiff.Section5.Field.mul_streamAnalyticMinimalResolventReal_one_eq {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : ↑mu * (streamWholeSpaceAnalyticData M omega).analyticMinimalResolventReal mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x = 1

The signed real stream resolvent has the exact constant-one normalization.

noncomputable def Algsuperdiff.Section5.Field.streamBallPart {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → ℝ

The centered function restricted to a ball by an indicator.

Equations

• Algsuperdiff.Section5.Field.streamBallPart f x r = (Metric.ball x r).indicator fun (y : HCPolySupport.Vec d) => f y - f x

noncomputable def Algsuperdiff.Section5.Field.streamComplementBallPart {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (r : ℝ) : HCPolySupport.Vec d → ℝ

The centered function restricted to the complement of a ball by an indicator.

Equations

• Algsuperdiff.Section5.Field.streamComplementBallPart f x r = (Metric.ball x r)ᶜ.indicator fun (y : HCPolySupport.Vec d) => f y - f x

theorem Algsuperdiff.Section5.Field.eventually_forall_abs_mul_streamAnalyticMinimalResolventReal_sub_lt {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hf : HasCompactSupport ⇑f) {eps : ℝ} (heps : 0 < eps) : ∀ᶠ (mu : ↑MarkovProcess.Semigroup.PositiveShift) in Filter.atTop, ∀ (x : HCPolySupport.Vec d), |↑mu * (streamWholeSpaceAnalyticData M omega).analyticMinimalResolventReal mu ⇑f ⋯ ⋯ x - f x| < eps

On compactly supported C₀ data, the normalized stream analytic minimal resolvent converges uniformly to the datum.

theorem Algsuperdiff.Section5.Field.tendsto_smul_streamAnalyticMinimalC0Resolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : Filter.Tendsto (fun (mu : ↑MarkovProcess.Semigroup.PositiveShift) => ↑mu • (streamWholeSpaceAnalyticData M omega).analyticMinimalC0ResolventOfVanishing ⋯ mu f) Filter.atTop (nhds f)

The stream-field analytic minimal C₀ resolvent is strongly normalized at large shifts.

theorem Algsuperdiff.Section5.Field.hasDenseRange_streamAnalyticMinimalC0 {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : (streamWholeSpaceAnalyticData M omega).HasDenseRangeAnalyticMinimalC0OfVanishing ⋯

Every operator in the stream analytic minimal C₀ resolvent has dense range.

noncomputable def Algsuperdiff.Section5.Field.streamAnalyticMinimalPositiveC0ContractiveResolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)

The model's split-skew analytic minimal resolver, assembled as a positive contractive C₀ resolvent. Its operator is definitionally the analytic minimal operator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Algsuperdiff.Section5.Field.streamAnalyticMinimalPositiveC0ContractiveResolvent_operator {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ((streamAnalyticMinimalPositiveC0ContractiveResolvent M omega).operator mu) f = (streamWholeSpaceAnalyticData M omega).analyticMinimalC0ResolventOfVanishing ⋯ mu f