IndisputableMonolith.Foundation.MeasureForcing

declarations in this module (62)

• def rho L130
• theorem rho_pos L132
• theorem rho_nonneg L136
• theorem rho_lt_one L138
• theorem rho_le_one L143
• theorem rho_ne_one L145
• theorem one_sub_rho L149
• def latticeWeight L157
• theorem latticeWeight_eq_rho_pow L159
• theorem latticeWeight_pos L161
• structure RecognitionWeightRule L173
• def toRungDilution L192
• theorem weight_forced L200
• theorem weight_unique L205
• def partitionZ L214
• theorem partitionZ_eq_phi_sq L220
• def probMass L226
• theorem probMass_pos L228
• theorem probMass_tsum_one L234
• theorem probMass_zero L242
• def meanRung L247
• theorem meanRung_eq_phi L251
• def Factorizes L278
• theorem f_zero L281
• theorem f_nmul L297
• theorem f_nonneg_of_nonneg L310
• theorem f_rat L320
• theorem f_ratCast L346
• theorem continuum_weight_forced L364
• def contWeight L438
• theorem contWeight_eq_phi_rpow_neg L441
• theorem contWeight_gibbs L449
• theorem contWeight_satisfies_premises L459
• theorem Jcost_exp_eq_cosh_sub_one L475
• lemma half_sq_le_cosh_sub_one_of_nonneg L480
• theorem half_sq_le_cosh_sub_one L495
• theorem sub_gaussian_in_J L507
• theorem theta_is_lattice_weight L521
• theorem hbar_is_lattice_weight L527
• theorem rung44_is_lattice_weight L536
• theorem kernel_dilution_is_measure L543
• structure LabeledState L564
• structure CostSufficientWeight L570
• theorem weight_blind_to_label L576
• theorem Jcost_phi_closed_form L588
• theorem Jcost_phi_gt_011 L595
• def saturation L600
• theorem saturation_closed L603
• theorem saturation_lt_one L611
• theorem saturation_monotone L616
• theorem saturation_tendsto_one L624
• def deltaW0 L641
• theorem deltaW0_lt_ceiling L644
• theorem deltaW0_tendsto_ceiling L651
• theorem rho_lt_06212 L658
• theorem deltaW0_gt_004 L667
• theorem rho_pow_nine_lt L681
• theorem deltaW0_near_ceiling L690
• theorem equilibrium_w0_band L707
• structure MeasureForcingCert L736
• def measureForcingCert L774
• theorem t9_measure_forced L798