Documentation

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

GradientScaleReadout #

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

Arbitrary-radius readout of the dyadic gradient iteration #

source
noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastGradientConstant (d : ℕ) :
ℝ

The dimension-only gradient-row constant in the divergence-source row.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastGradientConstant_nonneg (d : ℕ) :
    0 ≤ smallContrastGradientConstant d
    source
    def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.HasInteriorSmallContrastGradientScaleBound {d : ℕ} (alpha K : ℝ) (u : HCPolySupport.H1Function (smallContrastUnitBall d)) :
    Prop

    The local Morrey-gradient row used by Poincaré and Campanato.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.euclideanBall_subset_of_center_distance_add_lt {d : ℕ} {c z : HCPolySupport.Vec d} {r R : ℝ} (hr : 0 ≤ r) (hcz : HCPolySupport.euclideanNorm (z - c) + r ≤ R) :
      HCPolySupport.euclideanBall z r ⊆ HCPolySupport.euclideanBall c R

      Euclidean balls with a displaced centre remain in the ambient ball when the centre distance plus the inner radius is below the ambient radius.

      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.exists_smallContrastDyadicRadius_bracket {R s : ℝ} (hR : 0 < R) (hs : 0 < s) (hsR : s ≤ R) :
      ∃ (n : ℕ), smallContrastDyadicRadius R (n + 1) < s ∧ s ≤ smallContrastDyadicRadius R n
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.sqrt_volume_ratio_euclideanBall_le_half_rpow {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (_hst : s ≤ t) (hts : t ≤ 2 * s) :
      √((MeasureTheory.volume (HCPolySupport.euclideanBall z t)).toReal / (MeasureTheory.volume (HCPolySupport.euclideanBall z s)).toReal) ≤ (1 / 2) ^ (-↑d / 2)
      source
      theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.gradientScaleBound_of_dyadic {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {R alpha K : ℝ} (hR : 0 < R) (halpha1 : alpha < 1) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.MemVectorL2 (HCPolySupport.euclideanBall z R) g) (hdyadic : ∀ (n : ℕ), smallContrastDyadicRadius R n ^ (1 - alpha) * vectorNormalizedL2On (HCPolySupport.euclideanBall z (smallContrastDyadicRadius R n)) g ≤ K) (s : ℝ) :
      0 < s → s ≤ R → s ^ (1 - alpha) * vectorNormalizedL2On (HCPolySupport.euclideanBall z s) g ≤ (1 / 2) ^ (-↑d / 2) * K

      Arbitrary-radius consequence of an already assembled dyadic scale row.