| Name | Category | Theorems |
|---|
betaFromReal 📖 | CompOp | 4 mathmath: chain_rule_T_beta, deriv_beta_wrt_T, beta_fun_T_eq_on_Ioi, beta_fun_T_formula
|
instCoeNNReal 📖 | CompOp | — |
instCoeReal 📖 | CompOp | — |
instTopologicalSpace 📖 | CompOp | 1 mathmath: ofβ_continuousOn
|
instZero 📖 | CompOp | — |
ofNNReal 📖 | CompOp | 2 mathmath: ofNNReal_val, coe_ofNNReal_coe
|
ofRealNonneg 📖 | CompOp | 1 mathmath: ofRealNonneg_val
|
ofβ 📖 | CompOp | 13 mathmath: CanonicalEnsemble.log_partitionFunction_ofβ, CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_Z_of_beta, ofβ_eq, β_ofβ, CanonicalEnsemble.mathematicalPartitionFunction_comp_ofβ_apply, ofβ_differentiableOn, eventually_pos_ofβ, ofβ_β, CanonicalEnsemble.log_phys_eq_log_math_sub_const_on_Ioi, ofβ_continuousOn, tendsto_ofβ_atTop, tendsto_toReal_ofβ_atTop, CanonicalEnsemble.derivWithin_log_phys_eq_derivWithin_log_math
|
toReal 📖 | CompOp | 4 mathmath: coe_ofNNReal_real, eventually_pos_ofβ, tendsto_ofβ_atTop, tendsto_toReal_ofβ_atTop
|
val 📖 | CompOp | 18 mathmath: CanonicalEnsemble.fluctuation_dissipation_theorem_finite, chain_rule_T_beta, CanonicalEnsemble.heatCapacity_eq_deriv_meanEnergyBeta, deriv_beta_wrt_T, CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction, ext_iff, CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp, CanonicalEnsemble.helmholtzFreeEnergy_phase_space_unit_one, ofRealNonneg_val, ofβ_differentiableOn, CanonicalEnsemble.helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy, CanonicalEnsemble.helmholtzFreeEnergy_def, CanonicalEnsemble.fluctuation_dissipation_energy_parametric, CanonicalEnsemble.helmholtzFreeEnergy_dof_zero, CanonicalEnsemble.kB_mul_beta, ofNNReal_val, coe_ofNNReal_coe, CanonicalEnsemble.helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction
|
β 📖 | CompOp | 24 mathmath: CanonicalEnsemble.log_probability, CanonicalEnsemble.heatCapacity_eq_deriv_meanEnergyBeta, CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_mathZ_of_beta, CanonicalEnsemble.meanEnergy_eq_neg_deriv_log_Z_of_beta, CanonicalEnsemble.mathematicalPartitionFunction_eq_integral, CanonicalEnsemble.integral_energy_bolt, CanonicalEnsemble.twoState_meanEnergy_eq, CanonicalEnsemble.meanEnergy_eq_ratio_of_integrals, β_ofβ, CanonicalEnsemble.μBolt_of_fintype, CanonicalEnsemble.twoState_partitionFunction_apply_eq_cosh, CanonicalEnsemble.twoState_probability_snd, beta_pos, CanonicalEnsemble.twoState_probability_fst, ofβ_β, CanonicalEnsemble.kB_mul_beta, CanonicalEnsemble.partitionFunction_of_fintype, CanonicalEnsemble.mathematicalPartitionFunction_of_fintype, CanonicalEnsemble.differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ, CanonicalEnsemble.twoState_partitionFunction_apply, CanonicalEnsemble.integral_bolt_eq_integral_mul_exp, CanonicalEnsemble.derivWithin_meanEnergy_Beta_eq_neg_variance, CanonicalEnsemble.log_mathematicalPartitionFunction_eq, CanonicalEnsemble.derivWithin_log_phys_eq_derivWithin_log_math
|