Documentation

Lean 4 Proof

theorem ces_sextuple_role (ρ : ℝ) : SextupleRoleStatement J ρ where
  K_pos := fun hJ hρ => curvatureK_pos hJ hρ
  superadd := fun hJ hρ c hc v hv hv_ne =>
    ces_strict_concavity_on_perp hJ hρ hc v hv hv_ne
  corr_robust := fun hJ hρ m => diversity_encoding hJ hρ m
  strategic := fun hJ hρ c hc δ hδ hδ_ne =>
    ces_strict_concavity_on_perp hJ hρ hc δ hδ hδ_ne
  network := fun hJ hρne c hc =>
    network_scaling hJ hρne hc
  estimation := fun hρ c hc hJ => bridge_theorem hρ hc hJ
  phase := fun T Tstar => keff_eq_K_times_reduced J ρ T Tstar

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/QuadrupleRole.lean:80

Module Section

The CES Sextuple Role theorem (Paper 1, Section 9):

In the same file