Sections / Section 6: Information Geometry and Cumulant Tower / linearShareComponent

Linear Share Component

defprovedInfo Geometry

Documentation

Lean 4 Proof

def linearShareComponent (s0j s1j : ℝ) (t : ℝ) : ℝ :=
  (1 - t) * s0j + t * s1j

Dependency Graph

Used by

midpointDivergence no_shock_linear_trivial linear_at_zero discriminating_prediction_at_midpoint linear_at_one

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:525

Module Section

Information Geometry of CES:

In the same file

bregmanDiv welfare_eq_bregman klDivExp welfare_eq_kl kl_reverse welfareDistanceFn_deriv welfareDistanceFn_second_deriv fisherInfoExp welfare_curvature_is_fisher hessLogFEigenvalue hessLogF_from_cesEigenvalue escortFisherEigenvalue bridgeRatio bridge_theorem curvatureK_eq_bridge_times_fisher curvatureK_from_hessLogF fifth_role_of_K hierarchical_kl bridgeRatio_pos bridgeRatio_large_at_small_rho