TriadicRadii

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

Triadic radii and the geometric weight of a triadic Campanato telescope

The cubes of the underlying regularity theory have side 3 ^ j, so the Campanato telescope that reads a Hölder modulus out of an oscillation decay must step by the factor 3, not by the factor 2 of the textbook dyadic construction. This file collects the radius arithmetic of that telescope: the radii R 3 ^ (-k), the geometric ratio 3 ^ (-α) they contribute to a sum of α-weighted oscillations, and the sum of the resulting geometric series.

The exponent α is a free real parameter. Everything below needs only 0 < α, and the tail constant is kept in the exact closed form (1 - 3 ^ (-α))⁻¹; the numerical bound ≤ 3 is recorded separately for the range 1/2 ≤ α, where it is available, and is never used to define anything.

Main definitions

• triadicRadius R k — the radius R 3 ^ (-k).
• campanatoRatio α — the geometric ratio 3 ^ (-α) = (1/3) ^ α.
• campanatoTailConstant α — the sum (1 - 3 ^ (-α))⁻¹ of the geometric series.

Main results

• triadicRadius_rpow — the factorisation (R 3 ^ (-k)) ^ α = R ^ α (3 ^ (-α)) ^ k.
• exists_triadicRadius_bracket — every separation below R is bracketed by two consecutive radii.
• tendsto_triadicRadius_zero — the radii decrease to 0 from above.

1. The radii

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius (R : ℝ) (k : ℕ) : ℝ

The triadic radius R 3 ^ (-k).

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius R k = R * (1 / 3) ^ k

@[simp]

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_zero (R : ℝ) : triadicRadius R 0 = R

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_pos {R : ℝ} (hR : 0 < R) (k : ℕ) : 0 < triadicRadius R k

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_succ (R : ℝ) (k : ℕ) : triadicRadius R (k + 1) = triadicRadius R k / 3

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_le {R : ℝ} (hR : 0 ≤ R) (k : ℕ) : triadicRadius R k ≤ R

2. The geometric ratio

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRatio (alpha : ℝ) : ℝ

The geometric ratio 3 ^ (-α) of the α-weighted triadic telescope.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRatio alpha = (1 / 3) ^ alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRatio_lt_one {alpha : ℝ} (halpha : 0 < alpha) : campanatoRatio alpha < 1

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.one_sub_campanatoRatio_pos {alpha : ℝ} (halpha : 0 < alpha) : 0 < 1 - campanatoRatio alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.triadicRadius_rpow {R alpha : ℝ} (hR : 0 ≤ R) (k : ℕ) : triadicRadius R k ^ alpha = R ^ alpha * campanatoRatio alpha ^ k

The factorisation of the α-weight along the telescope.

3. The geometric tail

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoTailConstant (alpha : ℝ) : ℝ

The sum of the geometric series of ratio 3 ^ (-α). It is the only constant of the telescope that depends on the exponent, and it is kept in closed form.

Equations

• Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoTailConstant alpha = (1 - Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoRatio alpha)⁻¹

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoTailConstant_pos {alpha : ℝ} (halpha : 0 < alpha) : 0 < campanatoTailConstant alpha

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.campanatoTailConstant_le_three {alpha : ℝ} (halpha : 1 / 2 ≤ alpha) : campanatoTailConstant alpha ≤ 3

On the exponent range 1/2 ≤ α the tail constant is below the numerical value 3. Recorded for a consumer that prefers a numeral; the closed form is what the telescope uses.

4. Bracketing and the limit

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.exists_triadicRadius_bracket {R s : ℝ} (hR : 0 < R) (hs : 0 < s) (hsR : s ≤ R) : ∃ (k : ℕ), triadicRadius R (k + 1) < s ∧ s ≤ triadicRadius R k

Every separation in (0, R] lies between two consecutive triadic radii.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Campanato.tendsto_triadicRadius_zero {R : ℝ} (hR : 0 < R) : Filter.Tendsto (triadicRadius R) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))

The telescope radii tend to 0 through positive values.