Lemma S4: the mixture of stopped null distributions

This file proves Lemma S4 of the supplementary material, following its proof and that of Proposition S5, as the intermediate theorem lem_lbmix_of_duality, which takes as hypotheses the setting of Sections 1 and 2 and inequality (5) of Lemma 1 for the Gaussian null and the mixture Q, and Lemma S6 in the same form (lem_fixedk_of_duality).

• measurable_lbStoppingRule and isStoppingTime_lbStoppingRule: τ' is a stopping time of (ℱ_t) for every θ, measurable in (θ, x);
• measurable_lbRandomizedRule, isRandomizedStoppingTime_lbRandomizedRule, and lbMixture_mem_stoppedMixtures: τ is a randomized stopping time for each θ, so that P̄ ∈ ℬ;
• volume_lbRandomizedRule_eq: given (θ, X), τ stops at t_k with probability ½ 1(τ' = t_k) + ½ ξ_{t_k};
• lb_sum_lbWeights and lbWeights_mem_probVectors: ξ is uniform on {t₀, …, t_K};
• lbDensity and stoppedAlternative_eq_withDensity_lbDensity: Q^ξ has density ξ_t Π_t/J_k with respect to P̄ on {t} × ℝ^t for t = t_k, where Π_t = ∏_{i=2}^t ℓ(Y_i) (the notation of the proof of Proposition S5), by the density identity lb_lintegral_mixture_eq;
• lb_integrable_log_prod_lik and lb_integrable_log_lbJ: log Π_t and log{(K + 1)J_k} are Q-integrable, the latter since β' ≤ log{(K + 1)J_k} ≤ log{(K + 1)M} + x̄_t²/(2v₁) (lbJ_le_exp);
• klDiv_stoppedAlternative_lbMixture: KL(Q^ξ ‖ P̄) = ∑_k ξ_{t_k} E_Q{log(ξ_{t_k}Π_{t_k}/J_k)}, a nonnegative real number;
• lb_isEVariable_prod_lik: ∏_{i=2}^t ℓ(Y_i) ∈ ℰ_t, so that its e-power under Q is at most that of the numéraire;
• lem_lbmix_of_duality: Lemma S4;
• lem_fixedk_of_duality: Lemma S6.

For ρ² < 1 − s², the numéraires E*_t of Q need not be ∏_{i=2}^t ℓ(Y_i); as in the proof of Proposition S5, Lemma 1 is applied with E_Q(log E*_{t_k}) ≥ E_Q{log ∏_{i=2}^{t_k} ℓ(Y_i)}.

The stopping rule τ' and the randomized stopping time τ

theorem LogOptimal.measurable_lbZ_prod (t : ℕ) : Measurable fun (p : ℝ × (ℕ → ℝ)) => lbZ p.1 t p.2

theorem LogOptimal.measurableSet_lbStoppingRule_eq_coe {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c : ℝ) : MeasurableSet {p : ℝ × (ℕ → ℝ) | lbStoppingRule r K c p.1 p.2 = ↑(r ^ k)}

theorem LogOptimal.lbStoppingRule_eq_top_iff (r K : ℕ) (c θ : ℝ) (x : ℕ → ℝ) : lbStoppingRule r K c θ x = ⊤ ↔ ∀ k ≤ K, ¬(c ≤ |lbZ θ (r ^ k) x| ∧ |lbZ θ (r ^ k) x| ≤ c + 1)

theorem LogOptimal.lbStoppingRule_mem (r K : ℕ) (c θ : ℝ) (x : ℕ → ℝ) : lbStoppingRule r K c θ x = ⊤ ∨ ∃ k ≤ K, lbStoppingRule r K c θ x = ↑(r ^ k)

theorem LogOptimal.measurable_lbStoppingRule {r : ℕ} (hr : 2 ≤ r) (K : ℕ) (c : ℝ) : Measurable fun (p : ℝ × (ℕ → ℝ)) => lbStoppingRule r K c p.1 p.2

theorem LogOptimal.isStoppingTime_lbStoppingRule {r : ℕ} (hr : 2 ≤ r) (K : ℕ) (c θ : ℝ) : MeasureTheory.IsStoppingTime (dataFiltration ℝ) (lbStoppingRule r K c θ)

theorem LogOptimal.measurable_lbRandomizedRule {r : ℕ} (hr : 2 ≤ r) (K : ℕ) (c : ℝ) : Measurable fun (p : ℝ × (ℕ → ℝ) × ↑unitInterval) => lbRandomizedRule r K c p.1 p.2.1 p.2.2

theorem LogOptimal.isRandomizedStoppingTime_lbRandomizedRule {r : ℕ} (hr : 2 ≤ r) (K : ℕ) (c θ : ℝ) : IsRandomizedStoppingTime (lbRandomizedRule r K c θ)

theorem LogOptimal.lbMixture_mem_stoppedMixtures {r : ℕ} (hr : 2 ≤ r) (s ρ : ℝ) (K : ℕ) (c : ℝ) : lbMixture s ρ r K c ∈ stoppedMixtures gaussNull

Lemma S4, first claim: P̄ ∈ ℬ, since τ is a randomized stopping time for each θ.

The uniform randomization

theorem LogOptimal.lb_min_floor_eq_iff {K k : ℕ} (hk : k ≤ K) (u : ℝ) : ¬u < 1 / 2 ∧ min K ⌊(2 * u - 1) * (↑K + 1)⌋₊ = k ↔ 1 / 2 + ↑k / (2 * (↑K + 1)) ≤ u ∧ (k < K → u < 1 / 2 + (↑k + 1) / (2 * (↑K + 1)))

For k ≤ K and u ≥ 1/2, min{K, ⌊(2u − 1)(K + 1)⌋} = k exactly when u ∈ [1/2 + k/(2K + 2), 1/2 + (k + 1)/(2K + 2)), the upper bound only for k < K.

theorem LogOptimal.volume_lb_uniform_part {K k : ℕ} (hk : k ≤ K) : MeasureTheory.volume {u : ↑unitInterval | ¬↑u < 1 / 2 ∧ min K ⌊(2 * ↑u - 1) * (↑K + 1)⌋₊ = k} = ENNReal.ofReal (1 / (2 * (↑K + 1)))

The uniform part of τ stops at t_k, k ≤ K, with probability 1/(2K + 2).

theorem LogOptimal.volume_lbRandomizedRule_eq {r : ℕ} (hr : 2 ≤ r) {K k : ℕ} (hk : k ≤ K) (c θ : ℝ) (x : ℕ → ℝ) : MeasureTheory.volume {u : ↑unitInterval | lbRandomizedRule r K c θ x u = ↑(r ^ k)} = 2⁻¹ * {x : ℕ → ℝ | lbStoppingRule r K c θ x = ↑(r ^ k)}.indicator 1 x + 2⁻¹ * ENNReal.ofReal (1 / (↑K + 1))

The randomized stopping time (Section S1.6): given (θ, X), τ stops at t_k, k ≤ K, with probability ½ 1(τ' = t_k) + ½ ξ_{t_k}, where ξ_{t_k} = 1/(K + 1).

The weights ξ

theorem LogOptimal.lb_sum_lbWeights {M : Type u_1} [AddCommMonoid M] {r K T : ℕ} (hr : 2 ≤ r) (hKT : r ^ K ≤ T) (h : ℝ → ℕ → M) (h0 : ∀ (t : ℕ), h 0 t = 0) : ∑ t : Fin (T + 1), h (lbWeights r K T t) ↑t = ∑ k ∈ Finset.range (K + 1), h (1 / (↑K + 1)) (r ^ k)

A sum over t ≤ T with the weights ξ_t of lbWeights is a sum over the horizons t_k = r^k, k ≤ K.

theorem LogOptimal.lbWeights_mem_probVectors {r K T : ℕ} (hr : 2 ≤ r) (hKT : r ^ K ≤ T) : lbWeights r K T ∈ probVectors T

The density dQ^ξ/dP̄

noncomputable def LogOptimal.lbDensity (s ρ : ℝ) (r K : ℕ) (c : ℝ) (p : StoppedPath ℝ) : ENNReal

The density dQ^ξ/dP̄ of the proof of Lemma S4: ξ_t Π_t/J_k on {t} × ℝ^t for t = t_k, k ≤ K, with ξ_t = 1/(K + 1) and Π_t = ∏_{i=2}^t ℓ(Y_i), and zero elsewhere.

Equations

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

theorem LogOptimal.lb_measurable_runningMean_dataFiltration (t : ℕ) : Measurable (runningMean t)

theorem LogOptimal.lb_measurable_helmertVec_dataFiltration (t : ℕ) : Measurable (helmertVec t)

theorem LogOptimal.lb_measurable_lbJ_dataFiltration (s ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) : Measurable (lbJ s ρ r K c k)

theorem LogOptimal.lb_measurable_prod_lik_dataFiltration (s : ℝ) (t : ℕ) : Measurable fun (x : ℕ → ℝ) => ∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x)

theorem LogOptimal.lb_measurable_density_term (s ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) : Measurable fun (x : ℕ → ℝ) => ENNReal.ofReal ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x)

The density at t = t_k as a function of the path, ξ_t Π_t/J_k.

theorem LogOptimal.measurable_lbDensity (s ρ : ℝ) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) : Measurable (lbDensity s ρ r K c)

Q^ξ = P̄.withDensity g

theorem LogOptimal.lb_measurable_lbRandomizedRule' {r : ℕ} (hr : 2 ≤ r) (K : ℕ) (c : ℝ) : Measurable fun (q : (ℝ × (ℕ → ℝ)) × ↑unitInterval) => lbRandomizedRule r K c q.1.1 q.1.2 q.2

theorem LogOptimal.lb_ofReal_mul_div_cancel {a b c : ℝ} (ha : 0 ≤ a) (hb : 0 < b) (hc : 0 < c) : ENNReal.ofReal (a * b / c) * (ENNReal.ofReal c / ENNReal.ofReal b) = ENNReal.ofReal a

ξ_t Π_t/J_k × (J_k/Π_t) = ξ_t.

theorem LogOptimal.lb_indicator_lbDensity_mk (s ρ : ℝ) (r K : ℕ) (c : ℝ) {A : Set (StoppedPath ℝ)} (τ : ℕ∞) (x : ℕ → ℝ) : A.indicator (lbDensity s ρ r K c) (StoppedPath.mk τ x) = ∑ k ∈ Finset.range (K + 1), (if τ = ↑(r ^ k) then 1 else 0) * {x : ℕ → ℝ | StoppedPath.mk (↑(r ^ k)) x ∈ A}.indicator (fun (x : ℕ → ℝ) => ENNReal.ofReal ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x)) x

The integrand of ∫_A g dP̄ as a sum over the horizons t_k.

theorem LogOptimal.stoppedAlternative_eq_withDensity_lbDensity {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K T : ℕ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hKT : r ^ K ≤ T) {c : ℝ} (hc : 0 < c) : stoppedAlternative (mixAlt s ρ) T (lbWeights r K T) = (lbMixture s ρ r K c).withDensity (lbDensity s ρ r K c)

Q^ξ = P̄.withDensity g (proof of Lemma S4): dQ^ξ/dP̄ = ξ_t Π_t/J_k on {t} × ℝ^t for t = t_k, since, given (θ, X), τ stops at t_k with probability ½ 1(τ' = t_k) + ½ ξ_{t_k}, and ∫ E_θ[{½ 1(τ' = t_k) + ½ ξ_{t_k}} f] π(dθ) = E_Q(f J_k/Π_{t_k}) for ℱ_{t_k}-measurable f ≥ 0.

Integrability under Q

theorem LogOptimal.lb_mixAlt_map_helmertY {i : ℕ} (hi : 2 ≤ i) (s ρ : ℝ) : MeasureTheory.Measure.map (helmertY i) (mixAlt s ρ) = ProbabilityTheory.gaussianReal 0 (s ^ 2).toNNReal

Under Q, Y_i ∼ N(0, s²) for i ≥ 2.

theorem LogOptimal.lb_integrable_sq_helmertY {i : ℕ} (hi : 2 ≤ i) (s ρ : ℝ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => helmertY i x ^ 2) (mixAlt s ρ)

theorem LogOptimal.lb_integrable_log_prod_lik {s : ℝ} (hs : 0 < s) (ρ : ℝ) (t : ℕ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => Real.log (∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x))) (mixAlt s ρ)

log Π_t = ∑_{i=2}^t log ℓ(Y_i) is Q-integrable.

theorem LogOptimal.lbJ_le_exp {s ρ : ℝ} (hs : 0 < s) {r : ℕ} (hr : 1 ≤ r) (K : ℕ) (c : ℝ) (k : ℕ) (x : ℕ → ℝ) : lbJ s ρ r K c k x ≤ √(2 * Real.pi * (ρ ^ 2 + s ^ 2 / ↑(r ^ k))) / 2 * ((√(2 * Real.pi * (ρ ^ 2 + s ^ 2)))⁻¹ + 1 / (↑K + 1) * (√(2 * Real.pi * (ρ ^ 2 + s ^ 2 + 1 / ↑(r ^ k))))⁻¹) * Real.exp (runningMean (r ^ k) x ^ 2 / (2 * (ρ ^ 2 + s ^ 2 / ↑(r ^ k))))

An upper bound on J_k: J_k ≤ M exp{x̄_t²/(2v₁)} with v₁ = ρ² + s²/t and M = (2πv₁)^{1/2}{(2πγ²)^{-1/2} + ξ_t(2πv₂)^{-1/2}}/2, since ∫_{𝒵_k(y)} φ₁ ≤ 1 and φ_v ≤ (2πv)^{-1/2}.

theorem LogOptimal.lb_integrable_sq_runningMean {t : ℕ} (ht : 1 ≤ t) (s ρ : ℝ) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => runningMean t x ^ 2) (mixAlt s ρ)

theorem LogOptimal.lb_integrable_log_lbJ {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hc : 0 < c) {k : ℕ} (hk : k ≤ K) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => Real.log ((↑K + 1) * lbJ s ρ r K c k x)) (mixAlt s ρ)

log{(K + 1)J_k} is Q-integrable: it lies between β' (Lemma S5(i)) and log{(K + 1)M} + x̄_t²/(2v₁) (lbJ_le_exp).

The Kullback–Leibler divergence KL(Q^ξ ‖ P̄)

theorem LogOptimal.lbDensity_mk_pow {r : ℕ} (hr : 2 ≤ r) (s ρ : ℝ) (K : ℕ) (c : ℝ) {k : ℕ} (hk : k ≤ K) (x : ℕ → ℝ) : lbDensity s ρ r K c (StoppedPath.mk (↑(r ^ k)) x) = ENNReal.ofReal ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x)

theorem LogOptimal.lb_log_density_eq {K : ℕ} {P J : ℝ} (hP : 0 < P) (hJ : 0 < J) : Real.log (1 / (↑K + 1) * P / J) = Real.log P - Real.log ((↑K + 1) * J)

log(ξ_t Π_t/J_k) = log Π_t − log{(K + 1)J_k} with ξ_t = 1/(K + 1).

instance LogOptimal.instIsProbabilityMeasureStoppedPathRealLbMixture (s ρ : ℝ) (r K : ℕ) (c : ℝ) : MeasureTheory.IsProbabilityMeasure (lbMixture s ρ r K c)

The mixture P̄ is a probability measure.

theorem LogOptimal.lb_integrable_log_density_term {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hc : 0 < c) {k : ℕ} (hk : k ≤ K) : MeasureTheory.Integrable (fun (x : ℕ → ℝ) => Real.log ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x)) (mixAlt s ρ)

theorem LogOptimal.klDiv_stoppedAlternative_lbMixture {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {r K T : ℕ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hKT : r ^ K ≤ T) {c : ℝ} (hc : 0 < c) : InformationTheory.klDiv (stoppedAlternative (mixAlt s ρ) T (lbWeights r K T)) (lbMixture s ρ r K c) = ENNReal.ofReal (∑ k ∈ Finset.range (K + 1), 1 / (↑K + 1) * ∫ (x : ℕ → ℝ), Real.log ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x) ∂mixAlt s ρ) ∧ 0 ≤ ∑ k ∈ Finset.range (K + 1), 1 / (↑K + 1) * ∫ (x : ℕ → ℝ), Real.log ((1 / (↑K + 1) * ∏ i ∈ Finset.Icc 2 (r ^ k), lik s (helmertY i x)) / lbJ s ρ r K c k x) ∂mixAlt s ρ

The divergence in the proof of Lemma S4: KL(Q^ξ ‖ P̄) = ∑_k ξ_{t_k} E_Q{log(ξ_{t_k}Π_{t_k}/J_k)}, since dQ^ξ/dP̄ = ξ_t Π_t/J_k on {t} × ℝ^t for t = t_k; the sum is nonnegative by Gibbs' inequality.

Lemma S4

theorem LogOptimal.lb_isEVariable_prod_lik {s : ℝ} (hs : 0 < s) {t : ℕ} (ht : 1 ≤ t) : IsEVariable gaussNull t fun (x : ℕ → ℝ) => ENNReal.ofReal (∏ i ∈ Finset.Icc 2 t, lik s (helmertY i x))

Π_t = ∏_{i=2}^t ℓ(Y_i) ∈ ℰ_t for t ≥ 1: under P_θ, Y^t ∼ N(0, 1)^{⊗(t−1)}, and ∏_m ℓ(y_m) is the density of N(0, s²)^{⊗(t−1)} with respect to N(0, 1)^{⊗(t−1)}.

theorem LogOptimal.lb_sum_mul_regret_le_iSup {𝒳 : Type u_1} [MeasurableSpace 𝒳] {𝔓 : Set (MeasureTheory.Measure (ℕ → 𝒳))} {Q : MeasureTheory.Measure (ℕ → 𝒳)} {Es : ℕ → (ℕ → 𝒳) → ENNReal} (hS : Setting 𝔓 Q Es) {T : ℕ} {ξ : Fin (T + 1) → ℝ} (hξ : ξ ∈ probVectors T) {E : ℕ → (ℕ → 𝒳) → ENNReal} (hE : IsEProcess 𝔓 E) : ∑ t : Fin (T + 1), ↑(ξ t) * regret Q (Es ↑t) (E ↑t) ≤ ⨆ (t : ℕ), ⨆ (_ : t ≤ T), regret Q (Es t) (E t)

∑_t ξ_t R_t(E_t) ≤ max_{t ≤ T} R_t(E_t) for ξ ∈ Δ_T, since the regrets are nonnegative.

theorem LogOptimal.lem_lbmix_of_duality {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hS : Setting gaussNull (mixAlt s ρ) Es) (hduality : ∀ (T : ℕ), ∀ ξ ∈ probVectors T, ∀ (E : ℕ → (ℕ → ℝ) → ENNReal), IsEProcess gaussNull E → ∀ Pbar ∈ stoppedMixtures gaussNull, ∑ t : Fin (T + 1), ↑(ξ t) * ePower (mixAlt s ρ) (Es ↑t) - ↑(InformationTheory.klDiv (stoppedAlternative (mixAlt s ρ) T ξ) Pbar) ≤ ∑ t : Fin (T + 1), ↑(ξ t) * regret (mixAlt s ρ) (Es ↑t) (E ↑t)) {r K T : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hKT : r ^ K ≤ T) (hc : 0 < c) : lbMixture s ρ r K c ∈ stoppedMixtures gaussNull ∧ (↑(↑K + 1)⁻¹ * ∑ k ∈ Finset.range (K + 1), eIntegral (mixAlt s ρ) fun (x : ℕ → ℝ) => (ENNReal.ofReal ((↑K + 1) * lbJ s ρ r K c k x)).log) ≤ minimaxRegret gaussNull (mixAlt s ρ) Es T

Lemma S4 (lem:lbmix, Mixture of stopped null distributions), for every ρ > 0 and any numéraires Es of Q, from the setting of Sections 1 and 2 and inequality (5) of Lemma 1: P̄ ∈ ℬ and Γ_T ≥ (K + 1)^{-1} ∑_{k=0}^K E_Q[log{(K + 1)J_k}] (S8). Following the proof of Proposition S5, E_Q(log E*_{t_k}) ≥ E_Q(log Π_{t_k}) with Π_t = ∏_{i=2}^t ℓ(Y_i), by the log-optimality of the numéraire, and KL(Q^ξ ‖ P̄) = ∑_k ξ_{t_k} E_Q{log(ξ_{t_k}Π_{t_k}/J_k)}.

theorem LogOptimal.lem_fixedk_of_duality {s ρ : ℝ} (hs : 0 < s) (hs1 : s < 1) (hρ : 0 < ρ) {Es : ℕ → (ℕ → ℝ) → ENNReal} (hS : Setting gaussNull (mixAlt s ρ) Es) (hduality : ∀ (T : ℕ), ∀ ξ ∈ probVectors T, ∀ (E : ℕ → (ℕ → ℝ) → ENNReal), IsEProcess gaussNull E → ∀ Pbar ∈ stoppedMixtures gaussNull, ∑ t : Fin (T + 1), ↑(ξ t) * ePower (mixAlt s ρ) (Es ↑t) - ↑(InformationTheory.klDiv (stoppedAlternative (mixAlt s ρ) T ξ) Pbar) ≤ ∑ t : Fin (T + 1), ↑(ξ t) * regret (mixAlt s ρ) (Es ↑t) (E ↑t)) {r K T : ℕ} {c : ℝ} (hr : 4 ≤ r) (hK : 1 ≤ K) (hKT : r ^ K ≤ T) (hc : 0 < c) (hc' : 0 < lbCPrime r c) (hβ : lbBetaPrime s ρ ≤ lbBeta s ρ K c) : ↑(lbBeta s ρ K c - (lbBeta s ρ K c - lbBetaPrime s ρ) * ↑K * Real.exp (-lbCPrime r c ^ 2 / (2 * s ^ 2)) - (2 * (c + 1) / √(ρ ^ 2 + s ^ 2) + 2 * (c + 1) ^ 2 / (3 * √(ρ ^ 2 + s ^ 2) ^ 2)) / (↑K + 1)) ≤ minimaxRegret gaussNull (mixAlt s ρ) Es T

Lemma S6 (lem:fixedk), for every ρ > 0 and any numéraires Es of Q, from the setting of Sections 1 and 2 and inequality (5) of Lemma 1: inequality (S8) of Lemma S4 (lem_lbmix_of_duality) gives (S9) (lem_fixedk_of_lbmix).