theorem curvatureK_eq_bridge_times_fisher {J : ℕ} {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : c ≠ 0) (hJ : (↑J : ℝ) ≠ 0) :
    curvatureK J ρ =
    bridgeRatio ρ * (↑J - 1) * c ^ 2 * escortFisherEigenvalue J ρ c := by
  simp only [curvatureK, bridgeRatio, escortFisherEigenvalue]
  field_simp

theorem welfare_eq_bregman (z : ℝ) :
    welfareDistanceFn z =
    bregmanDiv (-Real.log z) (-Real.log 1) (-1) z 1 := by
  simp only [welfareDistanceFn, bregmanDiv, Real.log_one, neg_zero]
  ring

theorem hierarchical_kl {N : ℕ} (z : Fin N → ℝ) (hz : ∀ n, 0 < z n)
    (treeCoeff : Fin N → ℝ) :
    ∑ n : Fin N, treeCoeff n * welfareDistanceFn (z n) =
    ∑ n : Fin N, treeCoeff n * klDivExp (1 / z n) 1 := by
  congr 1; ext n
  rw [welfare_eq_kl (hz n)]

theorem fisherRaoDistance_self {J : ℕ} (s : Fin J → ℝ)
    (hs : ∀ j, 0 ≤ s j)
    (hsum : ∑ j : Fin J, s j = 1) :
    bhattacharyyaCoeff s s = 1 := by
  simp only [bhattacharyyaCoeff]
  simp_rw [Real.sqrt_mul_self (hs _)]
  exact hsum

theorem fisherRao_distance_invariance {J : ℕ} (s0 s1 : Fin J → ℝ) :
    fisherRaoDistance s0 s1 = Real.arccos (bhattacharyyaCoeff s0 s1) := rfl

theorem escortCumulant2_eq_variance [NeZero J]
    (x : Fin J → ℝ) (_hx : ∀ j, 0 < x j) (ρ : ℝ) :
    escortCumulant2 x ρ =
    escortVariance x ρ (fun j => Real.log (x j)) := by
  unfold escortCumulant2 escortVariance escortRawMoment
    escortPartitionZn escortExpectation escortProbability
  simp only [pow_one]
  simp_rw [div_mul_eq_mul_div, ← Finset.sum_div]

theorem cumulant3_is_derivative_of_variance [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    HasDerivAt (fun p => escortCumulant2 x p)
      (escortCumulant3 x ρ) ρ := by
  unfold escortCumulant2 escortCumulant3
  -- Get the moment recursion for M_2 and M_1
  have hM2 := escortRawMoment_hasDerivAt x hx ρ 2
  have hM1 := escortRawMoment_hasDerivAt x hx ρ 1
  -- Derivative of M_1^2 via chain rule
  have hM1sq := hM1.pow 2
  -- Combine: d/drho (M_2 - M_1^2) = dM_2 - d(M_1^2)
  have h := hM2.sub hM1sq
  refine h.congr_deriv ?_
  simp only [Nat.cast_ofNat]
  ring

theorem escortCumulant2_zero_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) :
    escortCumulant2 (fun _ : Fin J => c) ρ = 0 := by
  simp only [escortCumulant2, escortRawMoment_at_symmetry hc]
  ring

theorem prudence_locking [NeZero J]
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) (ρ : ℝ) :
    -- (i) kappa_3 is the derivative of kappa_2
    HasDerivAt (fun p => escortCumulant2 x p) (escortCumulant3 x ρ) ρ ∧
    -- (ii) Both vanish at symmetry
    (∀ c : ℝ, 0 < c →
      escortCumulant2 (fun _ : Fin J => c) ρ = 0 ∧
      escortCumulant3 (fun _ : Fin J => c) ρ = 0) :=
  ⟨cumulant3_is_derivative_of_variance x hx ρ,
   fun _ hc => ⟨escortCumulant2_zero_at_symmetry hc ρ,
                 escortCumulant3_zero_at_symmetry hc ρ⟩⟩

def compoundSymmetryCorr (r : ℝ) (J : ℕ) : ℝ :=
  (1 - r) / (1 + (↑J - 1) * r)

theorem crisis_correlation_dual {J : ℕ} (hJ : 2 ≤ J) :
    -- (i) Price limit: r = 0 gives cor = 1
    compoundSymmetryCorr 0 J = 1 ∧
    -- (ii) Quantity floor: cor > -1/(J-1) for all finite r
    (∀ r : ℝ, 0 ≤ r → -1 / (↑J - 1) < compoundSymmetryCorr r J) ∧
    -- (iii) Linear bound: beta = 1
    (∀ r : ℝ, 0 ≤ r → 1 - compoundSymmetryCorr r J ≤ ↑J * r) :=
  ⟨compoundSymmetryCorr_zero J,
   fun _ hr => correlation_above_floor hJ hr,
   fun _ hr => gap_from_one_le hJ hr⟩