feat: KL-UCB on gamma and exponential arms, and the rate function of the gamma family

LMLExplore/Bandits/AsymptoticOptimality.lean

@@ -33,7 +33,8 @@ prior has the same asymptotic upper bound on Gaussian bandits with variance `σ
 [LS, Theorem 36.3], so it is asymptotically optimal on these bandits too.
 
 More generally, let `ρ a` be a measure on `ℝ` for every arm `a`, all with the same set of means
-(one family for every arm, or Gaussian families with different known variances). On the bandits
+(one family for every arm, Gaussian families with different known variances, or gamma families
+with different known shapes, whose means are `(0, ∞)`). On the bandits
 whose arm `a` has a law in the exponential family of `ρ a`, the KL-UCB algorithm `klucbFam ρ` for
 these families [GC11; CGMMS13] is consistent, and its expected regret is `c* log n + o(log n)`
 with `c* = ∑_{a : Δ_a > 0} Δ_a / d_{ρ a}(μ_a, μ*)`, the Lai–Robbins constant of these bandits
@@ -81,6 +82,12 @@ an instance, on the Bernoulli bandits with means in `(0, 1)`.
 * `tendsto_klucbFam_gaussianReal_regret_div_log`,
   `isLittleO_klucbFam_gaussianReal_regret_sub_mul_log`: the Gaussian instance with known variances
   `σ2 a`, with `c* = ∑_{a : Δ_a > 0} 2 σ2_a / Δ_a`.
+* `tendsto_klucbFam_gammaMeasure_regret_div_log`,
+  `isLittleO_klucbFam_gammaMeasure_regret_sub_mul_log`: the instance of gamma arms with known
+  shapes `κ a`, with `c* = ∑_{a : Δ_a > 0} Δ_a / (κ_a (μ_a / μ* - 1 - log (μ_a / μ*)))`.
+* `tendsto_klucbFam_expMeasure_regret_div_log`, `isLittleO_klucbFam_expMeasure_regret_sub_mul_log`:
+  the instance of exponential arms, with
+  `c* = ∑_{a : Δ_a > 0} Δ_a / (μ_a / μ* - 1 - log (μ_a / μ*))`.
 * `expFamilyTS_jeffreysPrior_regret_eventually_le_of_mem_image_expFamily`: on a bandit whose arms
   are members of exponential families, where `μ*` is a mean of the family of every arm `a` with
   positive gap, `μ_a` a mean of the family of the best arm, the Jeffreys posteriors of the arms
@@ -406,6 +413,86 @@ theorem isLittleO_klucbFam_gaussianReal_regret_sub_mul_log (m : α → ℝ) {σ2
     ((eventually_gt_atTop 1).mono fun n hn ↦ (log_pos (by exact_mod_cast hn)).ne')
     (tendsto_klucbFam_gaussianReal_regret_div_log m hσ2 hν h)
 
+/-- **Asymptotic optimality of KL-UCB for gamma arms with known shapes.** Let the law of every arm
+`a` be the gamma law `gammaMeasure (κ a) (r a)` of shape `κ a > 0` and rate `r a > 0`, with mean
+`μ_a = κ a / r a`. The expected regret of the KL-UCB algorithm for the gamma families of shapes
+`κ a`, generated by any members `gammaMeasure (κ a) (s a)` with `s a > 0`, satisfies
+`E[R_n] / log n → ∑_{a : Δ_a > 0} Δ_a / (κ_a (μ_a / μ* - 1 - log (μ_a / μ*)))`, the Lai–Robbins
+constant of the gamma bandits with these shapes. -/
+theorem tendsto_klucbFam_gammaMeasure_regret_div_log {κ r : α → ℝ} (s : α → ℝ)
+    (hκ : ∀ a, 0 < κ a) (hs : ∀ a, 0 < s a) (hr : ∀ a, 0 < r a)
+    (hν : ∀ a, ν a = gammaMeasure (κ a) (r a))
+    (h : IsAlgEnvSeq O A R (klucbFam fun a ↦ gammaMeasure (κ a) (s a)) (Environment.bandit ν)
+      P) :
+    Tendsto (fun n : ℕ ↦ P[regret ν A n] / log n) atTop
+      (𝓝 (∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), gap ν a / (κ a *
+        ((ν a)[id] / (ν (bestArm ν))[id] - 1 - log ((ν a)[id] / (ν (bestArm ν))[id]))))) := by
+  -- Every gamma family of shape `κ a` has the means `(0, ∞)`, and `ν a` is one of its members.
+  have hmeans (a : α) : (gammaMeasure (κ a) (s a)).expFamilyMeans id = Set.Ioi 0 :=
+    expFamilyMeans_gammaMeasure (hκ a) (hs a)
+  have hmem (a : α) : ν a ∈ (gammaMeasure (κ a) (s a)).expFamily id ''
+      interior (integrableExpSet id (gammaMeasure (κ a) (s a))) := by
+    rw [image_expFamily_gammaMeasure (hκ a) (hs a), hν a]
+    exact ⟨r a, hr a, rfl⟩
+  have hpos (a : α) : 0 < (ν a)[id] := by
+    simp only [hν a, id_eq, TauCeti.Probability.integral_id_gammaMeasure (hκ a) (hr a)]
+    exact div_pos (hκ a) (hr a)
+  -- The constants agree term by term, by the closed form of the divergence of the gamma family.
+  convert tendsto_klucbFam_regret_div_log (fun a b ↦ (hmeans a).trans (hmeans b).symm) hmem h
+    using 3 with a
+  rw [expFamilyDiv_gammaMeasure (hκ a) (hs a) (hpos a) (hpos _)]
+
+/-- **Asymptotic optimality of KL-UCB for gamma arms with known shapes.** Let the law of every arm
+`a` be the gamma law `gammaMeasure (κ a) (r a)` of shape `κ a > 0` and rate `r a > 0`, with mean
+`μ_a = κ a / r a`. The expected regret of the KL-UCB algorithm for the gamma families of shapes
+`κ a`, generated by any members `gammaMeasure (κ a) (s a)` with `s a > 0`, is
+`c* log n + o(log n)`, where `c* = ∑_{a : Δ_a > 0} Δ_a / (κ_a (μ_a / μ* - 1 - log (μ_a / μ*)))` is
+the Lai–Robbins constant of the gamma bandits with these shapes. -/
+theorem isLittleO_klucbFam_gammaMeasure_regret_sub_mul_log {κ r : α → ℝ} (s : α → ℝ)
+    (hκ : ∀ a, 0 < κ a) (hs : ∀ a, 0 < s a) (hr : ∀ a, 0 < r a)
+    (hν : ∀ a, ν a = gammaMeasure (κ a) (r a))
+    (h : IsAlgEnvSeq O A R (klucbFam fun a ↦ gammaMeasure (κ a) (s a)) (Environment.bandit ν)
+      P) :
+    (fun n : ℕ ↦ P[regret ν A n] - (∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), gap ν a / (κ a *
+        ((ν a)[id] / (ν (bestArm ν))[id] - 1 - log ((ν a)[id] / (ν (bestArm ν))[id])))) * log n)
+      =o[atTop] fun n : ℕ ↦ log n :=
+  isLittleO_sub_mul_of_tendsto_div
+    ((eventually_gt_atTop 1).mono fun n hn ↦ (log_pos (by exact_mod_cast hn)).ne')
+    (tendsto_klucbFam_gammaMeasure_regret_div_log s hκ hs hr hν h)
+
+/-- **Asymptotic optimality of KL-UCB for exponential arms.** Let the law of every arm `a` be the
+exponential law `expMeasure (r a)` of rate `r a > 0`, with mean `μ_a = 1 / r a`. The expected
+regret of the KL-UCB algorithm for the exponential family, generated by any members
+`expMeasure (s a)` with `s a > 0`, satisfies
+`E[R_n] / log n → ∑_{a : Δ_a > 0} Δ_a / (μ_a / μ* - 1 - log (μ_a / μ*))`, the Lai–Robbins constant
+of the exponential bandits. -/
+theorem tendsto_klucbFam_expMeasure_regret_div_log {r : α → ℝ} (s : α → ℝ)
+    (hs : ∀ a, 0 < s a) (hr : ∀ a, 0 < r a) (hν : ∀ a, ν a = expMeasure (r a))
+    (h : IsAlgEnvSeq O A R (klucbFam fun a ↦ expMeasure (s a)) (Environment.bandit ν) P) :
+    Tendsto (fun n : ℕ ↦ P[regret ν A n] / log n) atTop
+      (𝓝 (∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), gap ν a /
+        ((ν a)[id] / (ν (bestArm ν))[id] - 1 - log ((ν a)[id] / (ν (bestArm ν))[id])))) := by
+  -- The exponential laws are the gamma laws of shape `1`.
+  simp only [expMeasure] at hν h
+  simpa only [one_mul] using
+    tendsto_klucbFam_gammaMeasure_regret_div_log (κ := fun _ ↦ 1) s (fun _ ↦ one_pos) hs hr hν h
+
+/-- **Asymptotic optimality of KL-UCB for exponential arms.** Let the law of every arm `a` be the
+exponential law `expMeasure (r a)` of rate `r a > 0`, with mean `μ_a = 1 / r a`. The expected
+regret of the KL-UCB algorithm for the exponential family, generated by any members
+`expMeasure (s a)` with `s a > 0`, is `c* log n + o(log n)`, where
+`c* = ∑_{a : Δ_a > 0} Δ_a / (μ_a / μ* - 1 - log (μ_a / μ*))` is the Lai–Robbins constant of the
+exponential bandits. -/
+theorem isLittleO_klucbFam_expMeasure_regret_sub_mul_log {r : α → ℝ} (s : α → ℝ)
+    (hs : ∀ a, 0 < s a) (hr : ∀ a, 0 < r a) (hν : ∀ a, ν a = expMeasure (r a))
+    (h : IsAlgEnvSeq O A R (klucbFam fun a ↦ expMeasure (s a)) (Environment.bandit ν) P) :
+    (fun n : ℕ ↦ P[regret ν A n] - (∑ a ∈ univ.filter (fun a ↦ 0 < gap ν a), gap ν a /
+        ((ν a)[id] / (ν (bestArm ν))[id] - 1 - log ((ν a)[id] / (ν (bestArm ν))[id]))) * log n)
+      =o[atTop] fun n : ℕ ↦ log n :=
+  isLittleO_sub_mul_of_tendsto_div
+    ((eventually_gt_atTop 1).mono fun n hn ↦ (log_pos (by exact_mod_cast hn)).ne')
+    (tendsto_klucbFam_expMeasure_regret_div_log s hs hr hν h)
+
 end ExpFamily
 
 section ExpFamilyTS

LMLExplore/Probability/Distributions/ExponentialFamily/Exponential.lean

@@ -22,7 +22,9 @@ value: the means of the family are the interval `(0, ∞)`, the natural paramete
 `r - μ⁻¹`, the member of mean `μ` is `expMeasure μ⁻¹`, and the divergence of the family in the mean
 parametrization is `d(μ, μ') = μ / μ' - 1 - log (μ / μ')`. In terms of the rates, the
 Kullback–Leibler divergence between `expMeasure r` and `expMeasure r'` is
-`r' / r - 1 - log (r' / r)`.
+`r' / r - 1 - log (r' / r)`. Its extension to every level, the Cramér rate function of the member
+of mean `μ`, is `dbar(x, μ) = x / μ - 1 - log (x / μ)` at levels `x > 0` and infinite at levels
+`x ≤ 0`; it determines the KL-UCB index of exponential rewards.
 
 Exponential arms are one of the parametric arm models of bandit identification, for example in
 A. Garivier and E. Kaufmann, *Optimal best arm identification with fixed confidence*, COLT 2016,
@@ -43,6 +45,13 @@ where the closed form of the divergence makes the transportation costs explicit.
   `d(μ, μ') = μ / μ' - 1 - log (μ / μ')` for `μ, μ' > 0`.
 * `LMLExplore.klDiv_expMeasure`: the Kullback–Leibler divergence between `expMeasure r` and
   `expMeasure r'` for `r, r' > 0` is `r' / r - 1 - log (r' / r)`.
+* `LMLExplore.image_expFamily_expMeasure`: the members of the family are the exponential laws
+  `expMeasure b` of rate `b > 0`.
+* `LMLExplore.expFamilyRate_expMeasure`, `LMLExplore.expFamilyRate_expMeasure_of_nonpos`: the
+  extended divergence is `dbar(x, μ) = x / μ - 1 - log (x / μ)` at levels `x > 0`, and `∞` at
+  levels `x ≤ 0`.
+* `LMLExplore.le_expFamilyUpper_expMeasure_iff`, `LMLExplore.expFamilyUpper_expMeasure_of_nonpos`:
+  the upper confidence level of the family at positive and at nonpositive levels.
 * `LMLExplore.tendsto_expFamilyDiv_expMeasure_nhdsGT_zero`,
   `LMLExplore.tendsto_expFamilyDiv_expMeasure_atTop`: `d(μ, μ') → ∞` as `μ'` tends to either
   endpoint `0` or `∞` of the means.
@@ -52,9 +61,11 @@ public section
 
 open MeasureTheory ProbabilityTheory InformationTheory Real Set Filter Topology
 
+open scoped ENNReal
+
 namespace LMLExplore
 
-variable {r η μ μ' : ℝ}
+variable {r η μ μ' x q : ℝ}
 
 /-- The member of natural parameter `η` of the exponential family of `expMeasure r` with statistic
 `id` is `expMeasure (r - η)`. For `η ≥ r`, both sides are the zero measure. -/
@@ -113,6 +124,43 @@ theorem klDiv_expMeasure {r' : ℝ} (hr : 0 < r) (hr' : 0 < r') :
     klDiv (expMeasure r) (expMeasure r') = ENNReal.ofReal (r' / r - 1 - log (r' / r)) := by
   rw [expMeasure, expMeasure, klDiv_gammaMeasure one_pos hr hr', one_mul]
 
+/-- The members of the exponential family of `expMeasure r` are the exponential laws `expMeasure b`
+of positive rate `b`. -/
+theorem image_expFamily_expMeasure (hr : 0 < r) :
+    (expMeasure r).expFamily id '' interior (integrableExpSet id (expMeasure r)) =
+      (fun b ↦ expMeasure b) '' Ioi 0 := by
+  simp only [expMeasure]
+  exact image_expFamily_gammaMeasure one_pos hr
+
+/-- At a level `x > 0`, the extended divergence of the exponential family of `expMeasure r` is
+`dbar(x, μ) = x / μ - 1 - log (x / μ)` for every mean `μ > 0`. -/
+@[simp]
+theorem expFamilyRate_expMeasure (hr : 0 < r) (hx : 0 < x) (hμ : 0 < μ) :
+    (expMeasure r).expFamilyRate id x μ = ENNReal.ofReal (x / μ - 1 - log (x / μ)) := by
+  rw [expMeasure, expFamilyRate_gammaMeasure one_pos hr hx hμ, one_mul]
+
+/-- At a level `x ≤ 0`, the extended divergence of the exponential family of `expMeasure r` is
+infinite for every mean `μ > 0`, since the exponential laws are supported on `(0, ∞)`. -/
+@[simp]
+theorem expFamilyRate_expMeasure_of_nonpos (hr : 0 < r) (hx : x ≤ 0) (hμ : 0 < μ) :
+    (expMeasure r).expFamilyRate id x μ = ∞ := by
+  rw [expMeasure, expFamilyRate_gammaMeasure_of_nonpos one_pos hr hx hμ]
+
+/-- The upper confidence level of the exponential family of `expMeasure r` at a level `x > 0`: for
+every `q ≥ x`, `q ≤ U(x, c)` if and only if `x / q - 1 - log (x / q) ≤ c`. This is the KL-UCB index
+of exponential rewards. -/
+theorem le_expFamilyUpper_expMeasure_iff (hr : 0 < r) (hx : 0 < x) (hxq : x ≤ q) {c : ℝ≥0∞} :
+    (q : EReal) ≤ (expMeasure r).expFamilyUpper id x c ↔
+      ENNReal.ofReal (x / q - 1 - log (x / q)) ≤ c := by
+  rw [expMeasure, le_expFamilyUpper_gammaMeasure_iff one_pos hr hx hxq, one_mul]
+
+/-- The upper confidence level of the exponential family of `expMeasure r` at a level `x ≤ 0` with
+a finite budget `c` is `U(x, c) = x`. -/
+@[simp]
+theorem expFamilyUpper_expMeasure_of_nonpos (hr : 0 < r) (hx : x ≤ 0) {c : ℝ≥0∞} (hc : c ≠ ∞) :
+    (expMeasure r).expFamilyUpper id x c = x := by
+  rw [expMeasure, expFamilyUpper_gammaMeasure_of_nonpos one_pos hr hx hc]
+
 /-- For a mean `μ > 0`, the divergence `d(μ, μ')` of the exponential family of `expMeasure r`
 tends to infinity as `μ'` tends to the endpoint `0` of the means. -/
 theorem tendsto_expFamilyDiv_expMeasure_nhdsGT_zero (hr : 0 < r) (hμ : 0 < μ) :

LMLExplore/Probability/Distributions/ExponentialFamily/Gamma.lean

@@ -5,7 +5,7 @@ Authors: LMLExplore contributors
 -/
 module
 
-public import LMLExplore.Probability.Distributions.ExponentialFamily.Mean
+public import LMLExplore.Probability.Distributions.ExponentialFamily.UpperConfidence
 public import TauCeti.Probability.Distributions.Gamma.Basic
 import LMLExplore.Analysis.SpecialFunctions.Log.Basic
 import TauCeti.Probability.Distributions.Tilted
@@ -26,6 +26,13 @@ the rates, the Kullback–Leibler divergence between `gammaMeasure a r` and `gam
 `a (r' / r - 1 - log (r' / r))`. For `r = 1`, the member `gammaMeasure a r'` of the family of
 `gammaMeasure a 1` has natural parameter `1 - r'`.
 
+Every positive level `x` is a mean, so the extended divergence `dbar(x, μ)`, the Cramér rate
+function of the member of mean `μ` at `x`, is `a (x / μ - 1 - log (x / μ))` there. At a level
+`x ≤ 0` it is infinite, since the gamma laws are supported on `(0, ∞)`. The upper confidence level
+`U(x, c)` of the family, the index of KL-UCB for gamma rewards of known shape `a`, is therefore
+characterized by `q ≤ U(x, c) ↔ a (x / q - 1 - log (x / q)) ≤ c` for `0 < x ≤ q`, and is `x` itself
+for `x ≤ 0` and a finite budget `c`.
+
 The exponential laws `expMeasure r = gammaMeasure 1 r` are the shape `a = 1`
 (`Probability/Distributions/ExponentialFamily/Exponential.lean`).
 
@@ -48,6 +55,14 @@ COLT 2016, where the closed form of the divergence makes the transportation cost
   `d(μ, μ') = a (μ / μ' - 1 - log (μ / μ'))` for `μ, μ' > 0`.
 * `LMLExplore.klDiv_gammaMeasure`: the Kullback–Leibler divergence between `gammaMeasure a r` and
   `gammaMeasure a r'` for `r, r' > 0` is `a (r' / r - 1 - log (r' / r))`.
+* `LMLExplore.image_expFamily_gammaMeasure`: the members of the family are the gamma laws
+  `gammaMeasure a b` of shape `a` and rate `b > 0`.
+* `LMLExplore.expFamilyRate_gammaMeasure`, `LMLExplore.expFamilyRate_gammaMeasure_of_nonpos`: the
+  extended divergence is `dbar(x, μ) = a (x / μ - 1 - log (x / μ))` at levels `x > 0`, and `∞` at
+  levels `x ≤ 0`.
+* `LMLExplore.le_expFamilyUpper_gammaMeasure_iff`,
+  `LMLExplore.expFamilyUpper_gammaMeasure_of_nonpos`: the upper confidence level of the family at
+  positive and at nonpositive levels.
 * `LMLExplore.tendsto_expFamilyDiv_gammaMeasure_nhdsGT_zero`,
   `LMLExplore.tendsto_expFamilyDiv_gammaMeasure_atTop`: `d(μ, μ') → ∞` as `μ'` tends to either
   endpoint `0` or `∞` of the means.
@@ -57,9 +72,11 @@ public section
 
 open MeasureTheory ProbabilityTheory InformationTheory Real Set Filter Topology
 
+open scoped ENNReal
+
 namespace LMLExplore
 
-variable {a r η μ μ' : ℝ}
+variable {a r η μ μ' x q : ℝ}
 
 /-- For `η < r`, the member of natural parameter `η` of the exponential family of
 `gammaMeasure a r` with statistic `id` is `gammaMeasure a (r - η)`. -/
@@ -167,6 +184,62 @@ theorem klDiv_gammaMeasure {r' : ℝ} (ha : 0 < a) (hr : 0 < r) (hr' : 0 < r') :
     div_div_cancel₀ ha.ne', expFamilyDiv_gammaMeasure ha hr (div_pos ha hr) (div_pos ha hr'),
     div_div_div_cancel_left' _ _ ha.ne'] at h
 
+/-- The members of the exponential family of `gammaMeasure a r` are the gamma laws
+`gammaMeasure a b` of shape `a` and positive rate `b`. -/
+theorem image_expFamily_gammaMeasure (ha : 0 < a) (hr : 0 < r) :
+    (gammaMeasure a r).expFamily id '' interior (integrableExpSet id (gammaMeasure a r)) =
+      (fun b ↦ gammaMeasure a b) '' Ioi 0 := by
+  rw [interior_integrableExpSet_id_gammaMeasure ha hr]
+  ext Q
+  constructor
+  · rintro ⟨η, hη, rfl⟩
+    exact ⟨r - η, sub_pos.2 hη, (expFamily_gammaMeasure ha hr hη).symm⟩
+  · rintro ⟨b, hb, rfl⟩
+    refine ⟨r - b, sub_lt_self r hb, ?_⟩
+    rw [expFamily_gammaMeasure ha hr (sub_lt_self r hb), sub_sub_cancel]
+
+/-- At a level `x > 0`, the extended divergence of the exponential family of `gammaMeasure a r` is
+`dbar(x, μ) = a (x / μ - 1 - log (x / μ))` for every mean `μ > 0`, since `x` is itself a mean. -/
+@[simp]
+theorem expFamilyRate_gammaMeasure (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) (hμ : 0 < μ) :
+    (gammaMeasure a r).expFamilyRate id x μ = ENNReal.ofReal (a * (x / μ - 1 - log (x / μ))) := by
+  rw [Measure.expFamilyRate_eq_ofReal_expFamilyDiv
+    (by rwa [expFamilyMeans_gammaMeasure ha hr]) (by rwa [expFamilyMeans_gammaMeasure ha hr]),
+    expFamilyDiv_gammaMeasure ha hr hx hμ]
+
+/-- At a level `x ≤ 0`, the extended divergence of the exponential family of `gammaMeasure a r` is
+infinite for every mean `μ > 0`: the member of mean `μ` is almost surely strictly positive, so
+every level `x ≤ 0` lies strictly below it almost surely and the rate function there is infinite. -/
+@[simp]
+theorem expFamilyRate_gammaMeasure_of_nonpos (ha : 0 < a) (hr : 0 < r) (hx : x ≤ 0)
+    (hμ : 0 < μ) : (gammaMeasure a r).expFamilyRate id x μ = ∞ := by
+  rw [Measure.expFamilyRate_def, expFamily_natParam_gammaMeasure ha hr hμ]
+  have := isProbabilityMeasure_gammaMeasure ha (div_pos ha hμ)
+  exact rateFunction_eq_top_of_ae_gt aemeasurable_id
+    ((TauCeti.Probability.ae_pos_gammaMeasure a (a / μ)).mono fun _ hy ↦ hx.trans_lt hy)
+
+/-- The upper confidence level of the exponential family of `gammaMeasure a r` at a level `x > 0`:
+for every `q ≥ x`, `q ≤ U(x, c)` if and only if `a (x / q - 1 - log (x / q)) ≤ c`. This is the
+KL-UCB index of rewards with gamma laws of known shape `a`. -/
+theorem le_expFamilyUpper_gammaMeasure_iff (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) (hxq : x ≤ q)
+    {c : ℝ≥0∞} : (q : EReal) ≤ (gammaMeasure a r).expFamilyUpper id x c ↔
+      ENNReal.ofReal (a * (x / q - 1 - log (x / q))) ≤ c := by
+  rw [Measure.le_expFamilyUpper_iff (not_ae_eq_const_gammaMeasure ha hr)
+    (by rw [expFamilyMeans_gammaMeasure ha hr]; exact hx.trans_le hxq) hxq,
+    expFamilyRate_gammaMeasure ha hr hx (hx.trans_le hxq)]
+
+/-- The upper confidence level of the exponential family of `gammaMeasure a r` at a level `x ≤ 0`
+with a finite budget `c` is `U(x, c) = x`: every mean is at infinite extended divergence from
+`x`. -/
+@[simp]
+theorem expFamilyUpper_gammaMeasure_of_nonpos (ha : 0 < a) (hr : 0 < r) (hx : x ≤ 0)
+    {c : ℝ≥0∞} (hc : c ≠ ∞) : (gammaMeasure a r).expFamilyUpper id x c = x := by
+  refine le_antisymm (Measure.expFamilyUpper_le_iff.2 ⟨le_rfl, fun q hq _ hqc ↦ ?_⟩)
+    (Measure.le_expFamilyUpper _ _ _ _)
+  rw [expFamilyMeans_gammaMeasure ha hr] at hq
+  rw [expFamilyRate_gammaMeasure_of_nonpos ha hr hx hq, top_le_iff] at hqc
+  exact absurd hqc hc
+
 /-- For a mean `μ > 0`, the divergence `d(μ, μ')` of the exponential family of `gammaMeasure a r`
 tends to infinity as `μ'` tends to the endpoint `0` of the means. -/
 theorem tendsto_expFamilyDiv_gammaMeasure_nhdsGT_zero (ha : 0 < a) (hr : 0 < r) (hμ : 0 < μ) :