Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib.

structure LongTails.OracleTemplate.GeneralizedAccelerated.ChargingState : Type

An active block and earlier blocks used to count curvature updates.

• active : ℕ × ℕ

  Start index and count of the active charging block.

• past : List (ℕ × ℕ)

  Completed charging blocks, in reverse chronological order.

def LongTails.OracleTemplate.GeneralizedAccelerated.charging (up : ℕ → Bool) : ℕ → ChargingState

Partition the iteration history into blocks starting at upward curvature changes.

Equations

• One or more equations did not get rendered due to their size.
• LongTails.OracleTemplate.GeneralizedAccelerated.charging up 0 = { active := (0, 0), past := [] }

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.chargeValue (w : ℕ → ℝ) (b : ℕ × ℕ) : ℝ

The exponentially weighted inverse-curvature mass of a block.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.chargeValue w b = 2 ^ b.2 * w b.1

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.chargeTotal (w : ℕ → ℝ) (s : ChargingState) : ℝ

The sum of the active and completed block charges.

Equations

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

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.downMass (up : ℕ → Bool) (w : ℕ → ℝ) (n : ℕ) : ℝ

The inverse-curvature mass accumulated at downward curvature changes.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.downMass up w n = ∑ i ∈ Finset.range (n + 1), if up i = true then 0 else w i

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_mass_succ (up : ℕ → Bool) (w : ℕ → ℝ) (n : ℕ) : downMass up w (n + 1) = downMass up w n + if up (n + 1) = true then 0 else w (n + 1)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_up {up : ℕ → Bool} (w : ℕ → ℝ) {n : ℕ} (h : up (n + 1) = true) : chargeValue w (charging up (n + 1)).active = 2 * w (n + 1) ∧ chargeTotal w (charging up (n + 1)) = chargeTotal w (charging up n) + 2 * w (n + 1)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_down {up : ℕ → Bool} (w : ℕ → ℝ) {n : ℕ} (h : up (n + 1) = false) : chargeValue w (charging up (n + 1)).active = 2 * chargeValue w (charging up n).active ∧ chargeTotal w (charging up (n + 1)) = chargeTotal w (charging up n) + chargeValue w (charging up n).active

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_potential {up : ℕ → Bool} {w : ℕ → ℝ} (hfirst : up 0 = false) (hw : ∀ (n : ℕ), 0 ≤ w n) (hnext : ∀ (n : ℕ), w (n + 1) = if up n = true then w n / 4 else 4 * w n) (n : ℕ) : chargeValue w (charging up n).active ≤ 16 * w n ∧ (up n = true → chargeValue w (charging up n).active = 2 * w n) ∧ chargeTotal w (charging up n) + 8 / 3 * w (n + 1) ≤ 16 * downMass up w n

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_total_le {up : ℕ → Bool} {w : ℕ → ℝ} (hfirst : up 0 = false) (hw : ∀ (n : ℕ), 0 ≤ w n) (hnext : ∀ (n : ℕ), w (n + 1) = if up n = true then w n / 4 else 4 * w n) (n : ℕ) : chargeTotal w (charging up n) ≤ 16 * downMass up w n

def LongTails.OracleTemplate.GeneralizedAccelerated.chargingEntries (s : ChargingState) : List (ℕ × ℕ)

The active block followed by all completed blocks.

Equations

• LongTails.OracleTemplate.GeneralizedAccelerated.chargingEntries s = s.active :: s.past

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_indices (up : ℕ → Bool) (n : ℕ) : (charging up n).active.1 ≤ n ∧ (∀ b ∈ (charging up n).past, b.1 < (charging up n).active.1) ∧ List.Pairwise (fun (a b : ℕ × ℕ) => b.1 < a.1) (chargingEntries (charging up n)) ∧ ∀ b ∈ chargingEntries (charging up n), b.1 = 0 ∨ up b.1 = true

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_index_le (up : ℕ → Bool) (n : ℕ) (b : ℕ × ℕ) (hb : b ∈ chargingEntries (charging up n)) : b.1 ≤ n

noncomputable def LongTails.OracleTemplate.GeneralizedAccelerated.chargePrefix (w : ℕ → ℝ) (s : ChargingState) (t : ℕ) : ℝ

The total charge from blocks whose start precedes a given iteration.

Equations

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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_prefix_bound {up : ℕ → Bool} {w B : ℕ → ℝ} (hB0 : 0 ≤ B 0) (hB : Monotone B) (htotal : ∀ (n : ℕ), chargeTotal w (charging up n) ≤ B n) (n : ℕ) (b : ℕ × ℕ) : b ∈ chargingEntries (charging up n) → chargePrefix w (charging up n) b.1 ≤ B b.1

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_count (up : ℕ → Bool) (n : ℕ) : (charging up n).active.2 + (List.map Prod.snd (charging up n).past).sum = n

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_nodup (up : ℕ → Bool) (n : ℕ) : (chargingEntries (charging up n)).Nodup

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_unique_index (up : ℕ → Bool) (n : ℕ) : Set.InjOn Prod.fst {b : ℕ × ℕ | b ∈ chargingEntries (charging up n)}

def LongTails.OracleTemplate.GeneralizedAccelerated.chargingSet (up : ℕ → Bool) (n : ℕ) : Finset (ℕ × ℕ)

The finite set of active and completed charging blocks.

Equations

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

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_sum (up : ℕ → Bool) (n : ℕ) (w : ℕ → ℝ) : ∑ b ∈ chargingSet up n, chargeValue w b = chargeTotal w (charging up n)

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_sum_count (up : ℕ → Bool) (n : ℕ) : ∑ b ∈ chargingSet up n, b.2 = n

theorem LongTails.OracleTemplate.GeneralizedAccelerated.charging_sum_prefix (up : ℕ → Bool) (n : ℕ) (w : ℕ → ℝ) (t : ℕ) : ∑ b ∈ chargingSet up n with b.1 < t, chargeValue w b = chargePrefix w (charging up n) t