Exhaustion

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

A spatial exhaustion function for the stream field

The reciprocal affine norm gives a positive, one-Lipschitz exhaustion of Vec d. Its compact superlevel sets control escape to spatial infinity. A radius amplification records the extra Euclidean separation forced when a distant point remains in a sufficiently high exhaustion superlevel set.

Main definitions

• streamExhaustionRho — the exhaustion (1 + ‖x‖)⁻¹.
• streamExhaustionAmp — the amplified radius used by spatial tail bounds.

noncomputable def Algsuperdiff.Section5.Field.streamExhaustionRho {d : ℕ} (x : HCPolySupport.Vec d) : ℝ

The reciprocal affine sup norm used to exhaust Vec d.

Equations

• Algsuperdiff.Section5.Field.streamExhaustionRho x = (1 + ‖x‖)⁻¹

theorem Algsuperdiff.Section5.Field.continuous_streamExhaustionRho {d : ℕ} : Continuous streamExhaustionRho

theorem Algsuperdiff.Section5.Field.streamExhaustionRho_pos {d : ℕ} (x : HCPolySupport.Vec d) : 0 < streamExhaustionRho x

theorem Algsuperdiff.Section5.Field.streamExhaustionRho_le_one {d : ℕ} (x : HCPolySupport.Vec d) : streamExhaustionRho x ≤ 1

theorem Algsuperdiff.Section5.Field.lipschitzWith_streamExhaustionRho {d : ℕ} : LipschitzWith 1 streamExhaustionRho

theorem Algsuperdiff.Section5.Field.isCompact_streamExhaustionRho_superlevel {d : ℕ} {eps : ℝ} (heps : 0 < eps) : IsCompact {x : HCPolySupport.Vec d | eps ≤ streamExhaustionRho x}

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

Increase a radius when its exhaustion scale forces additional separation.

Equations

• Algsuperdiff.Section5.Field.streamExhaustionAmp x r = if 4 * Algsuperdiff.Section5.Field.streamExhaustionRho x ≤ r then max r (2 / 3 * (1 + ‖x‖)) else r

theorem Algsuperdiff.Section5.Field.streamExhaustionAmp_pos {d : ℕ} {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) : 0 < streamExhaustionAmp x r

theorem Algsuperdiff.Section5.Field.streamExhaustionAmp_le_dist {d : ℕ} {x z : HCPolySupport.Vec d} {r : ℝ} (hdist : r ≤ dist z x) (hlevel : r - streamExhaustionRho x ≤ streamExhaustionRho z) : streamExhaustionAmp x r ≤ dist z x

The amplified radius of an exhaustion tail: a point Euclidean-far from x and in the superlevel set {rho ≥ r - rho x} is at distance at least the amplified radius from x.