Documentation

Lean 4 Proof

theorem escort_logit_bridge (x : Fin J → ℝ)
    (hx : ∀ j, 0 < x j) (ρ : ℝ) (j : Fin J) :
    escortDistribution J ρ x j =
    logitProbability J 1 (fun k => ρ * Real.log (x k)) j := by
  simp only [escortDistribution, logitProbability, div_one]
  have hrw : ∀ k, (x k) ^ ρ = Real.exp (ρ * Real.log (x k)) := fun k => by
    rw [rpow_def_of_pos (hx k), mul_comm]
  rw [hrw j]
  exact congrArg₂ (· / ·) rfl (Finset.sum_congr rfl fun k _ => hrw k)

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:325

Module Section

Ten Views of a Single Object:

In the same file