WhitneyWeightGeometric

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.whitneyDecayRatio : ℝ

The fixed geometric ratio left after paying the Whitney-layer growth.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.whitneyDecayRatio = 3 ^ (-(1 / 8))

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.whitneyDecayRatio_nonneg : 0 ≤ whitneyDecayRatio

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.whitneyDecayRatio_lt_one : whitneyDecayRatio < 1

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.norm_whitneyDecayRatio_lt_one : ‖whitneyDecayRatio‖ < 1

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.weighted_whitney_layer_factor_le {b gamma : ℝ} (hb0 : 0 ≤ b) (hb : b ≤ 1 / 64) (hgamma0 : 0 ≤ gamma) (hgamma : gamma ≤ b) (n g : ℕ) (hgap : g ≤ 2 * n + 1) : 3 ^ (-↑n / 4) * 3 ^ (2 * (b + gamma) * ↑g) ≤ 3 ^ (1 / 16) * whitneyDecayRatio ^ n

If b ≤ 1/64, gamma ≤ b, and the layer gap is at most 2n+1, then the growing factor spends at most half of the available 3^{-n/4} decay.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_succ_mul_whitneyDecayRatio : Summable fun (n : ℕ) => ↑(n + 1) * whitneyDecayRatio ^ n

Polynomially weighted copies of the fixed layer ratio are summable.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.hasSum_succ_mul_whitneyDecayRatio : HasSum (fun (n : ℕ) => ↑(n + 1) * whitneyDecayRatio ^ n) (1 / (1 - whitneyDecayRatio) ^ 2)

Exact geometric sum for the (n+1)-weighted layer ratio.