Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.Regularity.Ported.CampanatoGeometry

CampanatoGeometry #

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

Sup-ball geometry for the small-contrast Campanato readout #

The Campanato telescope is run on the ambient sup-balls. Their volume is exactly (2*r)^d, while the local gradient estimate is available on the containing Euclidean ball of radius d*r.

source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.euclideanBall_half_subset_unit_of_mem_half {d : ℕ} {z : HCPolySupport.Vec d} (hz : z ∈ smallContrastBall d (1 / 2)) :
HCPolySupport.euclideanBall z (1 / 2) ⊆ smallContrastUnitBall d
source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.metricBall_subset_euclideanBall_dimension {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) (r : ℝ) :
Metric.ball z r ⊆ HCPolySupport.euclideanBall z (↑d * r)

Every sup-ball of radius r is contained in the Euclidean ball of radius d*r.

source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_metricBall_toReal {d : ℕ} (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) :
(MeasureTheory.volume (Metric.ball z r)).toReal = (2 * r) ^ d

Real volume of a positive-radius sup-ball.

source
theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_metricBall_toReal_pos {d : ℕ} (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) :
0 < (MeasureTheory.volume (Metric.ball z r)).toReal
source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.metricToEuclideanVolumePrice (d : ℕ) :
ℝ

The exact normalized-volume price from a radius-r sup-ball to its Euclidean radius-d*r parent.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.metricToEuclideanVolumePrice_nonneg (d : ℕ) :
    0 ≤ metricToEuclideanVolumePrice d
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_volume_euclideanBall_dimension_div_metricBall {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) :
    √((MeasureTheory.volume (HCPolySupport.euclideanBall z (↑d * r))).toReal / (MeasureTheory.volume (Metric.ball z r)).toReal) = metricToEuclideanVolumePrice d
    source
    noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballVolumePrice (k : ℝ) (d : ℕ) :
    ℝ

    Normalized L² volume price for enlarging a sup-ball radius by k.

    Equations
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.ballVolumePrice_nonneg (k : ℝ) (d : ℕ) :
      0 ≤ ballVolumePrice k d
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_volume_metricBall_ratio {d : ℕ} (x y : HCPolySupport.Vec d) {R r k : ℝ} (hr : 0 < r) (hk : 0 < k) (hR : R = k * r) :
      √((MeasureTheory.volume (Metric.ball x R)).toReal / (MeasureTheory.volume (Metric.ball y r)).toReal) = ballVolumePrice k d

      Exact normalized-volume ratio for two sup-balls whose radii differ by a positive factor k; their centres may differ because Lebesgue volume is translation invariant.