IndisputableMonolith.Gravity.PageCurveOperatorEntropy

declarations in this module (18)

• def schmidtCapacityBound L38
• theorem schmidtCapacityBound_zero L45
• theorem schmidtCapacityBound_full L54
• theorem schmidtCapacityBound_at_page_fraction L62
• structure SchmidtSaturatedOperatorProcess L80
• theorem schmidtSaturated_entropy_eq_pageCurve L93
• theorem schmidtSaturated_entropy_zero L101
• theorem schmidtSaturated_entropy_full L109
• theorem schmidtSaturated_entropy_peak L118
• def canonicalSchmidtSaturatedProcess L136
• theorem schmidtSaturatedProcess_inhabited L151
• def operatorDerivedPageCurveProp L160
• theorem operatorDerivedPageCurveProp_holds L164
• def operatorPageCurveDerivedWitness L171
• structure PageCurveOperatorEntropyCert L180
• def pageCurveOperatorEntropyCert L188
• theorem pageCurveOperatorEntropyCert_inhabited L194
• theorem operator_page_curve_one_statement L203