CruxStreamPenalization

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

Fixed-collar localized penalization tails for the stream field

The collar used by exterior penalization is fixed once the killed cube is fixed. Hence the stream field's point-dependent algebraic amplitude and decay rate admit finite uniform bounds on that collar. This produces a single positive-rate log-subexponential error which tends to zero as the penalization mass grows. The comparison uses the localized split-skew tail and has no global small-contrast input.

def Algsuperdiff.Section5.Field.streamFixedCollarNormBound (v : ℕ) : ℝ

A uniform ambient-norm bound on the next exhaustion cube.

Equations

• Algsuperdiff.Section5.Field.streamFixedCollarNormBound v = 3 ^ (v + 1)

noncomputable def Algsuperdiff.Section5.Field.streamFixedCollarTailAmplitude {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : ℝ

A uniform amplitude for localized tails whose centers lie in the next exhaustion cube.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamFixedCollarTailRate {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : ℝ

A uniform positive decay rate for localized tails whose centers lie in the next exhaustion cube.

Equations

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

noncomputable def Algsuperdiff.Section5.Field.streamFixedCollarTailProfile {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : ℝ → ℝ

The uniform fixed-collar error profile.

Equations

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

theorem Algsuperdiff.Section5.Field.streamFixedCollarNormBound_nonneg (v : ℕ) : 0 ≤ streamFixedCollarNormBound v

theorem Algsuperdiff.Section5.Field.norm_le_streamFixedCollarNormBound {d v : ℕ} {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d (v + 1)) : ‖x‖ ≤ streamFixedCollarNormBound v

theorem Algsuperdiff.Section5.Field.streamFixedCollarTailAmplitude_nonneg {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : 0 ≤ streamFixedCollarTailAmplitude M omega v

theorem Algsuperdiff.Section5.Field.streamFixedCollarTailRate_pos {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : 0 < streamFixedCollarTailRate M omega v

theorem Algsuperdiff.Section5.Field.streamLocalizedTailProfile_le_fixedCollar {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d (v + 1)) (s : ℝ) : streamLocalizedTailProfile M omega x s ≤ streamFixedCollarTailProfile M omega v s

On the next exhaustion cube the pointwise localized profile is bounded by the fixed-collar profile.

theorem Algsuperdiff.Section5.Field.tendsto_streamFixedCollarTailProfile_atTop {d : ℕ} (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v : ℕ) : Filter.Tendsto (streamFixedCollarTailProfile M omega v) Filter.atTop (nhds 0)

Every positive-rate fixed-collar profile tends to zero at infinity.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPenalizedCube_le_next_add_localizedTail_of_subset {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (L : WholeSpaceLocalizedSplitData A) (tailError : ℝ) (htailError : 0 ≤ tailError) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (v : ℕ) (hVcube : V ⊆ wholeSpaceCube d v) (n k : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ V → f x = 0) (htailUniform : ∀ y ∈ wholeSpaceCube d (v + 1), L.tail ⟨↑mu + ↑n, ⋯⟩ y 1 ≤ tailError) {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d v) : A.analyticPenalizedCubeResolvent hV n mu f hf hf1 (k + (v + 2)) x ≤ A.analyticPenalizedCubeResolvent hV n mu f hf hf1 (v + 1) x + tailError / ↑mu

A coefficient-generic comparison driven by a localized tail bound which is uniform on the fixed collar. No small-contrast datum is assumed.

theorem Algsuperdiff.Section5.Field.streamLocalizedSplitData_tail_unit_le_fixedCollar {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (v n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {y : HCPolySupport.Vec d} (hy : y ∈ DivergenceFormProcess.Form.wholeSpaceCube d (v + 1)) (hsqrt : 1 < √(↑mu + ↑n)) : (streamLocalizedSplitData M omega).tail ⟨↑mu + ↑n, ⋯⟩ y 1 ≤ streamFixedCollarTailProfile M omega v √(↑mu + ↑n)

At sufficiently large penalization mass, the stream localized tail on a unit ball centered in the fixed collar is controlled by one uniform profile.

theorem Algsuperdiff.Section5.Field.streamAnalyticPenalizedCube_le_next_add_fixedCollarTail_of_subset {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (v : ℕ) (hVcube : V ⊆ DivergenceFormProcess.Form.wholeSpaceCube d v) (n k : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ V → f x = 0) (hsqrt : 1 < √(↑mu + ↑n)) {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d v) : (streamWholeSpaceAnalyticData M omega).analyticPenalizedCubeResolvent hV n mu f hf hf1 (k + (v + 2)) x ≤ (streamWholeSpaceAnalyticData M omega).analyticPenalizedCubeResolvent hV n mu f hf hf1 (v + 1) x + streamFixedCollarTailProfile M omega v √(↑mu + ↑n) / ↑mu

The far-cube penalized stream resolvent is bounded by the next-cube resolvent plus the fixed-collar localized tail. This is the stream-field, small-contrast-free successor of the original Agmon comparison.

theorem Algsuperdiff.Section5.Field.toReal_streamAnalyticPenalizedResolvent_le_next_add_fixedCollarTail_of_subset {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (v : ℕ) (hVcube : V ⊆ DivergenceFormProcess.Form.wholeSpaceCube d v) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) (hfsupp : ∀ᵐ (x : HCPolySupport.Vec d), x ∉ V → f x = 0) (hsqrt : 1 < √(↑mu + ↑n)) {x : HCPolySupport.Vec d} (hx : x ∈ DivergenceFormProcess.Form.wholeSpaceCube d v) : ((streamWholeSpaceAnalyticData M omega).analyticPenalizedResolvent hV n mu f hf hf1 x).toReal ≤ (streamWholeSpaceAnalyticData M omega).analyticPenalizedCubeResolvent hV n mu f hf hf1 (v + 1) x + streamFixedCollarTailProfile M omega v √(↑mu + ↑n) / ↑mu

Passing the stream fixed-collar comparison to the exhaustion supremum.