CampanatoTelescope

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

The Campanato telescope on [1/2,1)

The exponent is restricted to [1/2,1) because the unrestricted Campanato constant is of order alpha⁻¹. Consequently the dyadic ratio 2^{-alpha} is uniformly below 3/4, so the geometric tail costs at most 4, independently of alpha.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.abs_volumeAverage_sub_windowAverage_le {d : ℕ} {W V : Set (HCPolySupport.Vec d)} (hVm : MeasurableSet V) (hsub : V ⊆ W) (hWpos : 0 < (MeasureTheory.volume W).toReal) (hVpos : 0 < (MeasureTheory.volume V).toReal) (hVtop : MeasureTheory.volume V ≠ ⊤) {f : HCPolySupport.Vec d → ℝ} (hfV : MeasureTheory.IntegrableOn f V MeasureTheory.volume) (hfV2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (f x - HCPolySupport.volumeAverage W f) ^ 2) V MeasureTheory.volume) (hfW2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (f x - HCPolySupport.volumeAverage W f) ^ 2) W MeasureTheory.volume) : |HCPolySupport.volumeAverage V f - HCPolySupport.volumeAverage W f| ≤ √((MeasureTheory.volume W).toReal / (MeasureTheory.volume V).toReal) * Section4.Support.normalizedL2On W fun (x : HCPolySupport.Vec d) => f x - HCPolySupport.volumeAverage W f

The difference of averages on nested windows is controlled by the normalized oscillation on the larger window.

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRatio (alpha : ℝ) : ℝ

The dyadic contraction ratio for the Campanato oscillation estimate.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRatio alpha = (1 / 2) ^ alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRatio_nonneg (alpha : ℝ) : 0 ≤ smallContrastCampanatoRatio alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRatio_lt_one {alpha : ℝ} (halpha : 0 < alpha) : smallContrastCampanatoRatio alpha < 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRatio_le_three_quarters {alpha : ℝ} (halpha : 1 / 2 ≤ alpha) : smallContrastCampanatoRatio alpha ≤ 3 / 4

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.inv_one_sub_smallContrastCampanatoRatio_le_four {alpha : ℝ} (halpha : 1 / 2 ≤ alpha) : (1 - smallContrastCampanatoRatio alpha)⁻¹ ≤ 4

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastDyadicRadius_rpow {R alpha : ℝ} (hR : 0 ≤ R) (n : ℕ) : smallContrastDyadicRadius R n ^ alpha = R ^ alpha * smallContrastCampanatoRatio alpha ^ n

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoAverage {d : ℕ} (u : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) (n : ℕ) : ℝ

The averages over shrinking dyadic balls used to construct a pointwise representative.

Equations

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

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastCampanatoRepresentative {d : ℕ} (u : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

The pointwise representative obtained as the limit of dyadic Campanato averages.

Equations

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

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.metricBall_dyadic_subset_unit {d : ℕ} [NeZero d] {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) (n : ℕ) : Metric.ball x (smallContrastDyadicRadius (smallContrastCampanatoRadius d) n) ⊆ smallContrastUnitBall d

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dist_smallContrastCampanatoAverage_succ_le {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (hcamp : HasSmallContrastBallCampanatoBound alpha K u) {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) (n : ℕ) : dist (smallContrastCampanatoAverage u.toFun x n) (smallContrastCampanatoAverage u.toFun x (n + 1)) ≤ ballVolumePrice 2 d * smallContrastCampanatoConstant d * K * smallContrastCampanatoRadius d ^ alpha * smallContrastCampanatoRatio alpha ^ n

Consecutive means differ by the Campanato oscillation on the parent ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.cauchySeq_smallContrastCampanatoAverage {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) : CauchySeq (smallContrastCampanatoAverage u.toFun x)

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.tendsto_smallContrastCampanatoAverage {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) : Filter.Tendsto (smallContrastCampanatoAverage u.toFun x) Filter.atTop (nhds (smallContrastCampanatoRepresentative u.toFun x))

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.dist_average_representative_le {d : ℕ} [NeZero d] {alpha K : ℝ} {u : HCPolySupport.H1Function (smallContrastUnitBall d)} (halpha : alpha ∈ Set.Ico (1 / 2) 1) (hK : 0 ≤ K) (hcamp : HasSmallContrastBallCampanatoBound alpha K u) {x : HCPolySupport.Vec d} (hx : x ∈ smallContrastBall d (1 / 2)) (n : ℕ) : dist (smallContrastCampanatoAverage u.toFun x n) (smallContrastCampanatoRepresentative u.toFun x) ≤ 4 * ballVolumePrice 2 d * smallContrastCampanatoConstant d * K * smallContrastDyadicRadius (smallContrastCampanatoRadius d) n ^ alpha

Uniform tail of the dyadic mean telescope. On [1/2,1) the order-alpha⁻¹ denominator is bounded by the literal factor 4.