{ "case_id": "MG-C003", "version": "0.1.1", "items": [ { "id": "CH03-D01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.I_const" }, { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.I_id" }, { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.I_act" } ], "representation": "定义受限子集上的常值分量、恒等分量与有效分量，按常值优先排除交集", "dependencies": [] }, { "id": "CH03-D02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.Fib" } ], "representation": "受限子集上关于指标子族J在复合伪度量下以y为目标的计算纤维", "dependencies": [] }, { "id": "CH03-D03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.R_eq" }, { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.R_zero" }, { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.fiber_preorder" } ], "representation": "算子在受限域上的点值相等点对集、全分量零距点对集，以及由包含诱导的纤维预序", "dependencies": [] }, { "id": "CH03-D04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.r_null" } ], "representation": "给定输入与输出伪度量下，基点y围绕计算纤维的内切开球上确界半径", "dependencies": [] }, { "id": "CH03-D05", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.r_null_uniform" }, { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.null_matrix_entry" } ], "representation": "基点集A在评估域U上的统一零化半径（点态半径inf），以及全分量零化矩阵条目", "dependencies": [ "CH03-D04" ] }, { "id": "CH03-D06", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.diam" }, { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.IsMonotoneScale" }, { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.classify_channel" } ], "representation": "输入尺度函数族（包含默认直径上确界）与两项二值阈值分类", "dependencies": [ "CH03-D05" ] }, { "id": "CH03-D07", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.IsTotallyBounded" } ], "representation": "基于冻结基础模块的内覆盖数与度量熵，定义正精度有限覆盖的全有界接口", "dependencies": [] }, { "id": "CH03-D08", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.entropy_diff" } ], "representation": "两端子族在正精度下的映射熵差，取值于扩展实数，反映覆盖熵变化", "dependencies": [ "CH03-D07" ] }, { "id": "CH03-P01-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_1_i" } ], "representation": "常值分量输出距离恒为0，等价于系数全为0的零行Lip上界", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P01-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_1_ii" } ], "representation": "常值分量且存在正输入距离的源分量，合法co-Lip矩阵条目必为0", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P01-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_1_iii" } ], "representation": "恒等分量输出输入双向三角不等式放缩，证明输出距离等于输入距离", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P02-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_2_i" } ], "representation": "两步复合算子在中间像域上的有效分量包含关系，逆否分为四种情况", "dependencies": [ "CH03-D01", "CH03-P01-03" ] }, { "id": "CH03-P02-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_2_ii" } ], "representation": "有限链对长度归纳，基例单位算子有效分量为空，归纳步应用两步包含", "dependencies": [ "CH03-D01", "CH03-P02-01" ] }, { "id": "CH03-P02-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_2_iii" } ], "representation": "恒等分量在复合下的交集包含，利用双向保距严格排除常值优先分支", "dependencies": [ "CH03-D01", "CH03-P01-03" ] }, { "id": "CH03-P03-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.remark_3_2_counterexample" } ], "representation": "两点对换算子在距离1伪度量下，验证两单步有效但自复合恒等，严格否定两条逆向包含", "dependencies": [ "CH03-D01", "CH03-P02-01", "CH03-P02-03" ] }, { "id": "CH03-P04-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_3_i" } ], "representation": "外侧算子在内侧实际像域上常值，复合输入点代入即得复合算子常值", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P04-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.prop_3_3_ii_counterexample" } ], "representation": "七点双分量模型验证：内侧i分量归零，但外侧输出在i分量上具有距离1正分离", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P05-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComponentPartition.lean", "name": "OperatorLocalDegeneracy.cor_3_4" } ], "representation": "外侧算子指定行除对角外全0，内侧常值使得复合输出距离为L*0=0，系数允许为无穷", "dependencies": [ "CH03-D01" ] }, { "id": "CH03-P06-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_i" } ], "representation": "两目标在子族复合伪度量下零距，由三角不等式证明对应计算纤维集合严格相等", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P06-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_ii_a" } ], "representation": "对每个像点y，自身原像自距为0使纤维非空，且并集恰好覆盖U", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P06-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_ii_b" } ], "representation": "两纤维若有交点，由交点作为中介证明两目标零距，从而纤维相等；否则不交", "dependencies": [ "CH03-D02", "CH03-P06-01" ] }, { "id": "CH03-P06-04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_iii" } ], "representation": "上确界为0等价于所有分量同时为0，建立子族纤维与单分量纤维交集的严格等式", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P06-05", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_iv" } ], "representation": "子族增大时包含更多分量零距约束，纤维集合单调收缩", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P06-06", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_v" } ], "representation": "单元素子族纤维化简为单分量点集，全指标集纤维包含于每个分量纤维", "dependencies": [ "CH03-D02", "CH03-P06-05" ] }, { "id": "CH03-P06-07", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_vi_a" } ], "representation": "恒等分量下输出目标零距双向等价于输入与目标零距", "dependencies": [ "CH03-D01", "CH03-D02" ] }, { "id": "CH03-P06-08", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_5_vi_b" } ], "representation": "常值分量在像目标的纤维为全集U，而在正距离目标处的纤维为空集", "dependencies": [ "CH03-D01", "CH03-D02" ] }, { "id": "CH03-P07-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_6_i_nec" } ], "representation": "点值像映射T存在时，同输入像点经T变换必产生相等输出，蕴含相等关系包含", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P07-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_6_i_suff" } ], "representation": "由相等关系包含利用选择公理选取原像代表元，构造良定映射T满足复合等式", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P07-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_6_ii" } ], "representation": "双向应用必要性与充分性，证明双向变换存在当且仅当相等点对集相等", "dependencies": [ "CH03-D03", "CH03-P07-01", "CH03-P07-02" ] }, { "id": "CH03-P07-04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_6_iii" } ], "representation": "有限正KA逆向放缩结合LB正向Lip放缩，在实际像域上得到LB/KA标量界", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P08-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_7_one_way" } ], "representation": "零距商映射存在等价于零距关系包含，利用原像代表元证明代表元无关与公式成立", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P08-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_7_two_way" } ], "representation": "双向商映射存在当且仅当零距点对集完全相等", "dependencies": [ "CH03-D03", "CH03-P08-01" ] }, { "id": "CH03-P08-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_7_separating" } ], "representation": "两像集分离时全分量零距等价于点相等，将商判据等价转回点值判据", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P09-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_9_refl_trans" } ], "representation": "固定评估域U上的纤维预序具有自反性与传递性", "dependencies": [ "CH03-D03" ] }, { "id": "CH03-P09-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_9_chain" } ], "representation": "有限链任意两层之间的关系包含由单步包含传递归纳得到", "dependencies": [ "CH03-D03", "CH03-P09-01" ] }, { "id": "CH03-P09-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ComputationalFibers.lean", "name": "OperatorLocalDegeneracy.prop_3_9_strict" } ], "representation": "单步真包含提取差集见证点，推出整条链首尾两端的零距点对集真包含", "dependencies": [ "CH03-D03", "CH03-P09-02" ] }, { "id": "CH03-P10-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.rbot_metric" }, { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.step_op" } ], "representation": "实数带隔离吸收元的标准度量与阶跃算子，定义对称去心评估域U", "dependencies": [ "CH03-D04" ] }, { "id": "CH03-P10-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_counterexample" } ], "representation": "每个y∈U的合法正半径恰为(0,|y|]，上确界给出点态半径|y|>0", "dependencies": [ "CH03-D04", "CH03-P10-01" ] }, { "id": "CH03-P10-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_counterexample" } ], "representation": "取趋零基点序列证明固定域U上的统一半径下确界严格为0", "dependencies": [ "CH03-D05", "CH03-P10-02" ] }, { "id": "CH03-P11-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_8_i_a" } ], "representation": "输出子族常值时，任意两像点全分量零距，像目标计算纤维等于全域U", "dependencies": [ "CH03-D01", "CH03-D02" ] }, { "id": "CH03-P11-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_8_i_b_ptwise" }, { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_8_i_b_uniform" } ], "representation": "纤维为U使所有有限正半径均合法，点态与统一零化半径均为正无穷", "dependencies": [ "CH03-D04", "CH03-D05", "CH03-P11-01" ] }, { "id": "CH03-P11-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_8_ii_counterexample" } ], "representation": "两点无穷输入距离模型，统一半径为无穷但输出分量具有正距离非同值", "dependencies": [ "CH03-D01", "CH03-D05" ] }, { "id": "CH03-P12-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_9_i" } ], "representation": "恒等分量在像目标的计算纤维化简为基点在输入伪度量下的零距类", "dependencies": [ "CH03-D01", "CH03-D02", "CH03-P06-07" ] }, { "id": "CH03-P12-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_9_ii" } ], "representation": "开球内仅含输入零距点时，r0为合法内切半径，推出点态零化半径≥r0>0", "dependencies": [ "CH03-D01", "CH03-D04", "CH03-P12-01" ] }, { "id": "CH03-P13-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_10_ptwise_min" } ], "representation": "点态子族零化半径等于各分量零化半径的有限非空下确界最小值", "dependencies": [ "CH03-D04", "CH03-P06-04" ] }, { "id": "CH03-P13-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_10_uniform_min" } ], "representation": "交换基点集合上的下确界与有限非空指标集的最小值，得到统一半径公式", "dependencies": [ "CH03-D05", "CH03-P13-01" ] }, { "id": "CH03-P13-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_10_antimono" } ], "representation": "目标子族包含J⊆K导致对更大指标集取min，统一零化半径反向单调不增", "dependencies": [ "CH03-D05", "CH03-P13-02" ] }, { "id": "CH03-P14-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_11_fiber_zero" } ], "representation": "输入落入以像为目标的计算纤维直接蕴含输出分量距离为0", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P14-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_11_lt_sSup" } ], "representation": "输入距离严格小于点态上确界半径，提取介于中间的合法正半径推出输出零距", "dependencies": [ "CH03-D04" ] }, { "id": "CH03-P14-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_11_compose_inst" } ], "representation": "两步复合算子在中间像域上的单步纤维截断判据实例", "dependencies": [ "CH03-D02", "CH03-P14-01" ] }, { "id": "CH03-P15-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_12_i" } ], "representation": "下游在实际中间像域上保持零距时，复合统一零化半径不小于内侧零化半径", "dependencies": [ "CH03-D05", "CH03-P14-02" ] }, { "id": "CH03-P15-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_12_ii" } ], "representation": "内侧具有单通道Lip界L，下游像域统一半径除以L给出复合统一半径下界", "dependencies": [ "CH03-D05", "CH03-P14-02" ] }, { "id": "CH03-P16-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.lemma_3_13_exhaustive" }, { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.lemma_3_13_exclusive" } ], "representation": "四种二值阈值组合互斥且穷尽", "dependencies": [ "CH03-D06" ] }, { "id": "CH03-P16-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.lemma_3_13_i" } ], "representation": "输入尺度阈值增大时，严格小于阈值的输入通道集合单调不减", "dependencies": [ "CH03-D06" ] }, { "id": "CH03-P16-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.lemma_3_13_ii" } ], "representation": "零化阈值增大时，统一零化半径大于等于阈值的通道集合单调不增", "dependencies": [ "CH03-D06" ] }, { "id": "CH03-P17-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.prop_3_14_i" } ], "representation": "单调输入尺度在子集收缩时单调减小，保持严格小于尺度阈值结论", "dependencies": [ "CH03-D06" ] }, { "id": "CH03-P17-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.prop_3_14_ii_a" } ], "representation": "固定基点在收缩后的子集上考察，合法开球条件更容易满足，点态半径不减", "dependencies": [ "CH03-D04" ] }, { "id": "CH03-P17-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.prop_3_14_ii_b" } ], "representation": "基点集合收缩与点态半径单调递增共同保证统一零化半径单调不减", "dependencies": [ "CH03-D05", "CH03-P17-02" ] }, { "id": "CH03-P17-04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ThresholdClassification.lean", "name": "OperatorLocalDegeneracy.prop_3_14_iii" } ], "representation": "单点集直径为0严格小于阈值，但超集两点集直径为1大于阈值，否定反向推导", "dependencies": [ "CH03-D06" ] }, { "id": "CH03-P18-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_15_i" } ], "representation": "输入距离严格低于统一零化半径，放缩到基点点态半径后应用单步判据推出输出零距", "dependencies": [ "CH03-D05", "CH03-P14-02" ] }, { "id": "CH03-P18-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_15_ii" } ], "representation": "输出正分离由逆否命题直接推出输入距离大于等于统一零化半径", "dependencies": [ "CH03-D05", "CH03-P18-01" ] }, { "id": "CH03-P18-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/NullificationRadius.lean", "name": "OperatorLocalDegeneracy.prop_3_15_iii" } ], "representation": "统一半径低于阈值时，对介于中间的α提取见证两点与有限正ε，含无穷输出距离", "dependencies": [ "CH03-D05" ] }, { "id": "CH03-P19-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_i" } ], "representation": "统一零化半径不小于阈值时，以每个点为中心的阈值开球全部包含于对应的计算纤维", "dependencies": [ "CH03-D05", "CH03-P18-01" ] }, { "id": "CH03-P19-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_ii_a" } ], "representation": "输入端有限内覆盖中心集的像集构成输出端任意精度的内覆盖，给出覆盖数不等式", "dependencies": [ "CH03-D05", "CH03-D07", "CH03-P19-01" ] }, { "id": "CH03-P19-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_ii_b" } ], "representation": "由覆盖数不等式取以2为底的对数，推得对应度量熵的单调性不等式", "dependencies": [ "CH03-D07", "CH03-P19-02" ] }, { "id": "CH03-P20-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_16_counterexample" } ], "representation": "在阶跃反例上任意有限正τ选取对称二点集，输入覆盖数为1而输出在1/2尺度覆盖数为2", "dependencies": [ "CH03-D07", "CH03-P10-02" ] }, { "id": "CH03-P21-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.cor_3_17_i" } ], "representation": "在输入直径严格小于两阈值的前提下，证明统一半径达到阈值等价于输出整体零距", "dependencies": [ "CH03-D05", "CH03-D06", "CH03-P18-01" ] }, { "id": "CH03-P21-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.cor_3_17_ii" } ], "representation": "非空集整体输出零距时，单中心开球覆盖整个像集，内部覆盖数恰为1", "dependencies": [ "CH03-D07", "CH03-P21-01" ] }, { "id": "CH03-P22-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.remark_entropy_diff_well_defined" } ], "representation": "非空有限输入集及其像集的覆盖数均受有限基数控制，度量熵有限实数，熵差良定", "dependencies": [ "CH03-D08" ] }, { "id": "CH03-P23-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_18_i" } ], "representation": "常值分量输出覆盖数为1且熵为0，映射熵差恒等于输入端度量熵", "dependencies": [ "CH03-D01", "CH03-D08", "CH03-P21-02" ] }, { "id": "CH03-P23-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_18_ii_a" } ], "representation": "恒等分量前向推中心与反向选原像双向等距控制，证明覆盖数与度量熵严格相等", "dependencies": [ "CH03-D01", "CH03-D07", "CH03-P01-03" ] }, { "id": "CH03-P23-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_18_ii_b" } ], "representation": "在度量熵有限良定前提下，恒等分量覆盖数相等直接推出映射熵差为0", "dependencies": [ "CH03-D08", "CH03-P23-02" ] }, { "id": "CH03-P24-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_19_i" } ], "representation": "标量Lip常数L将ε/L内覆盖推为像集ε内覆盖，证明覆盖数单调上界", "dependencies": [ "CH03-D07" ] }, { "id": "CH03-P24-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_19_ii" } ], "representation": "输入全有界推出两端熵有限，代入覆盖数不等式给出映射熵差下界", "dependencies": [ "CH03-D07", "CH03-D08", "CH03-P24-01" ] }, { "id": "CH03-P25-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_20_i" } ], "representation": "正有限co-Lip矩阵条目将像集ε内覆盖拉回为输入ε/K内覆盖，给出覆盖数下界", "dependencies": [ "CH03-D07" ] }, { "id": "CH03-P25-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/CoveringEntropy.lean", "name": "OperatorLocalDegeneracy.prop_3_20_ii" } ], "representation": "输入端全有界保证输入熵有限，覆盖数下界取对数推出映射熵差上界", "dependencies": [ "CH03-D07", "CH03-D08", "CH03-P25-01" ] }, { "id": "CH03-P26-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_i_a_extended" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_i_a_fiber" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_i_a_const" } ], "representation": "验证绝对值读数伪度量公理，计算单步仿射算子在0的纤维为全集U，分量属于常值分量", "dependencies": [ "CH03-D01", "CH03-D02" ] }, { "id": "CH03-P26-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_i_b_fiber" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_i_b_act" } ], "representation": "自复合算子在0处的纤维严格退化为单点集{0}，分量属于有效分量", "dependencies": [ "CH03-D01", "CH03-D02" ] }, { "id": "CH03-P26-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_1_ii" } ], "representation": "点值常算子在输入集上取同一常数，自复合后两点输出重合，计算纤维仍为全集U无法区分", "dependencies": [ "CH03-D02" ] }, { "id": "CH03-P27-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_2_i" } ], "representation": "正co-Lip通道与点态零化判据共同作用，严格证明开区间(0,rN)内无输入距离点", "dependencies": [ "CH03-D04", "CH03-P14-02" ] }, { "id": "CH03-P27-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_2_ii" } ], "representation": "统一零化半径为正时，域内任意两点输入距离必须为0或大于等于统一半径", "dependencies": [ "CH03-D05", "CH03-P27-01" ] }, { "id": "CH03-P28-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/ Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_3_i_id_fiber" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_3_i_trans_fiber" } ], "representation": "习题 3.3 (i) 完整列出恒等算子与平移算子在U上的计算纤维分划", "dependencies": [ "CH03-D02", "CH03-P26-01" ] }, { "id": "CH03-P28-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_3_cov_U" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_3_cov_phi_U" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_3_entropy_diff" } ], "representation": "习题 3.3 (ii) 在精度3/2下精确计算两端内部覆盖数与映射熵差", "dependencies": [ "CH03-D07", "CH03-D08", "CH03-P28-01" ] }, { "id": "CH03-P29-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.diam_Da" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.r_null_unif_Da" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.type_Da" } ], "representation": "习题 3.4 (i-a) 计算D=[0,1/2]的直径1/2、统一半径⊤及阈值类型(1,1)", "dependencies": [ "CH03-D06", "CH03-D05" ] }, { "id": "CH03-P29-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.diam_Db" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.r_null_unif_Db" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.type_Db" } ], "representation": "习题 3.4 (i-b) 计算D=[9/10,11/10]的直径1/5、统一半径0及阈值类型(1,0)", "dependencies": [ "CH03-D06", "CH03-D05" ] }, { "id": "CH03-P29-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.diam_Dc" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.r_null_unif_Dc" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.type_Dc" } ], "representation": "习题 3.4 (i-c) 计算D={0,2}的直径2、统一半径2及阈值类型(0,1)", "dependencies": [ "CH03-D06", "CH03-D05" ] }, { "id": "CH03-P29-04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.diam_Dd" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.r_null_unif_Dd" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.type_Dd" } ], "representation": "习题 3.4 (i-d) 计算D=[0,2]的直径2、统一半径0及阈值类型(0,0)", "dependencies": [ "CH03-D06", "CH03-D05", "CH03-P29-02" ] }, { "id": "CH03-P29-05", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex_3_4_ii_counterexample" } ], "representation": "习题 3.4 (ii) 由D={0,2}反例否定无直径条件时统一半径≥1即整体零化", "dependencies": [ "CH03-P29-03" ] }, { "id": "CH03-P30-01", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_gt_2" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_1_to_2" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_le_1" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_center_3_2_not_in_U" } ], "representation": "习题 3.5 (i) 四点集在所有有限正ε下的分段覆盖数及3/2不是内部中心说明", "dependencies": [ "CH03-D07" ] }, { "id": "CH03-P30-02", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_f_image" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_g_image" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_f_image" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_g_image" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_entropy_diff_f" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_entropy_diff_g" } ], "representation": "习题 3.5 (ii) f与g像集重排为原集、各精度覆盖数相同且映射熵差为0", "dependencies": [ "CH03-D08", "CH03-P30-01" ] }, { "id": "CH03-P30-03", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_f_lip" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_f_lip_lower" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_g_lip" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_g_lip_lower" } ], "representation": "习题 3.5 (iii-a) 分别证明f的最优Lip常数为1和g的最优Lip常数为3及必要下界", "dependencies": [ "CH03-D07" ] }, { "id": "CH03-P30-04", "status": "complete", "declarations": [ { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_cov_at_7_4" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_bound_f_at_7_4" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_bound_g_at_7_4" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_compare_f" }, { "file": "OperatorLocalDegeneracy/Exercises.lean", "name": "OperatorLocalDegeneracy.ex35_compare_g" } ], "representation": "习题 3.5 (iii-b) 在ε=7/4代入一般上界与真实覆盖数逐项比较", "dependencies": [ "CH03-P30-01", "CH03-P30-02", "CH03-P30-03" ] } ] }