BaseLoss

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

Basic A for the Section 3.2 Option-A base loss

Algsuperdiff.Section3.baseLoss d s = 1 + 6 d (log 3) / s is the adopted all-scale loss of the Section 3.2 base case, defined on the literal source range 0 < s < 1.

This file records the small facts that downstream base-case estimates need: the loss is at least one, hence positive, and it is antitone in the multiscale regularity parameter s.

References

• ABK26, Section 3.2.

theorem Algsuperdiff.Section3.Provider.Scales.baseLoss_eq (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : baseLoss d s = 1 + 6 * ↑d * Real.log 3 / ↑s

The defining formula of the Option-A base loss.

theorem Algsuperdiff.Section3.Provider.Scales.one_le_baseLoss (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : 1 ≤ baseLoss d s

The Option-A base loss is a genuine loss: it is at least one.

theorem Algsuperdiff.Section3.Provider.Scales.baseLoss_pos (d : ℕ) (s : { s : ℝ // s ∈ Set.Ioo 0 1 }) : 0 < baseLoss d s

The Option-A base loss is strictly positive.

theorem Algsuperdiff.Section3.Provider.Scales.sqrt_baseLoss_le (d : ℕ) (u : { s : ℝ // s ∈ Set.Ioo 0 1 }) : √(baseLoss d u) ≤ √(1 + 6 * ↑d * Real.log 3) * (↑u)⁻¹

The Option-A base loss has a square root of size K / s with a dimension-only K: on 0 < s < 1 one has baseLoss d s <= (1 + 6 d log 3) s^{-2}.