IndisputableMonolith.NumberTheory.AnnularCost

declarations in this module (43)

• def phiCost L43
• theorem phiCost_zero L46
• theorem phiCost_symm L50
• theorem phiCost_nonneg L54
• def kappa L59
• theorem kappa_pos L61
• theorem phiCost_quadratic_lb L68
• theorem phiCost_eq_Jcost L107
• theorem phiCost_convexOn L114
• def phiCostLinearCoeff L126
• def phiCostQuadraticCoeff L130
• theorem abs_exp_sub_one_sub_id_le_sq_of_abs_le_one L134
• theorem cosh_sub_one_le_sq_of_abs_le_one L140
• theorem abs_sinh_le_abs_add_sq_of_abs_le_one L172
• theorem phiCost_add_le_phiCost_add_linear_quadratic L210
• structure AnnularRingSample L299
• def ringCost L305
• structure AnnularMesh L309
• def annularCost L315
• theorem jensen_ring_bound L323
• theorem ring_coercivity L368
• def topologicalFloor L388
• theorem ringCost_ge_topologicalFloor L392
• theorem ringCost_le_topologicalFloor_add_linear_quadratic_error L405
• def annularTopologicalFloor L464
• def annularExcess L468
• theorem annular_coercivity L474
• theorem harmonic_sum_diverges L498
• structure RegularCarrier L520
• structure AnnularTrace L527
• structure BudgetedCarrier L540
• def carrierBudgetScale L549
• theorem carrierBudgetScale_nonneg L553
• theorem carrier_budget L566
• theorem topologicalFloor_nonneg L572
• theorem topologicalFloor_zero L579
• theorem annularTopologicalFloor_nonneg L584
• theorem annularTopologicalFloor_zero L592
• theorem annularTopologicalFloor_le_annularCost L600
• theorem annularExcess_nonneg L610
• theorem topologicalFloor_pos_of_charge_ne_zero L616
• theorem annularTopologicalFloor_one_pos_of_charge_ne_zero L638
• theorem excess_bounded L648