Discharging HasFinePartitions

Concrete controls admit arbitrarily fine partitions: the linear control on ℝ via uniform subdivision (the workhorse), controls dominated by a fine one, and powers of fine controls.

theorem RoughPaths.Sewing.HasFinePartitions.of_le {T : Type u} [Preorder T] {ω η : Control T} (h : HasFinePartitions η) (hle : ∀ ⦃s t : T⦄, s ≤ t → ω.toFun s t ≤ η.toFun s t) : HasFinePartitions ω

A control dominated by one with fine partitions has fine partitions.

theorem RoughPaths.Sewing.HasFinePartitions.constMul {T : Type u} [Preorder T] {ω : Control T} (h : HasFinePartitions ω) {c : ENNReal} (hc : c ≠ ⊤) : HasFinePartitions (Control.constMul c ω)

Scalar multiples of controls with fine partitions have fine partitions.

theorem RoughPaths.Control.ofReal_hasFinePartitions {c : ENNReal} (hc : c ≠ ⊤) : Sewing.HasFinePartitions (ofReal c)

The linear control on ℝ admits fine partitions (uniform subdivision).

theorem RoughPaths.Sewing.HasFinePartitions.rpow {T : Type u} [Preorder T] {ω : Control T} (h : HasFinePartitions ω) {p : ℝ} (hp : 1 ≤ p) : HasFinePartitions (ω.rpow p hp)

Powers of fine controls are fine.