import formal_oet.vol_01.ch_01_foundations.gauge_space import formal_oet.vol_01.ch_01_foundations.operator_space import formal_oet.vol_01.ch_01_foundations.metric_entropy import OperatorLocalDegeneracy.ComponentPartition import OperatorLocalDegeneracy.ComputationalFibers import Mathlib.Data.ENNReal.Basic import Mathlib.Data.Real.Basic namespace OperatorLocalDegeneracy set_option linter.unusedSectionVars false set_option linter.unusedTactic false set_option linter.unreachableTactic false set_option linter.unusedVariables false open formal_oet.vol_01.ch_01_foundations variable {X I : Type} {bot : X} [Fintype I] [DecidableEq I] variable (d : I → X → X → ENNReal) /-- CH03-D04: 点态零化内切半径 -/ noncomputable def r_null (ϕ : Operator X bot) (d_in d_out : X → X → ENNReal) (y : X) (U : Set X) : ENNReal := sSup { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d_in x y < r → d_out (ϕ.func x) (ϕ.func y) = 0 } /-- CH03-D05: 统一零化半径 -/ noncomputable def r_null_uniform (ϕ : Operator X bot) (d_in d_out : X → X → ENNReal) (A U : Set X) : ENNReal := ⨅ y ∈ A, r_null ϕ d_in d_out y U /-- CH03-D05: 零化矩阵条目 -/ noncomputable def null_matrix_entry (ϕ : Operator X bot) (U : Set X) (j i : I) : ENNReal := r_null_uniform ϕ (d i) (d j) U U /-- CH03-P11-01: 命题 3.8 (i-a) 输出子族常值时每个像目标纤维等于U -/ theorem prop_3_8_i_a (ϕ : Operator X bot) (U : Set X) (J : Set I) (hJ : J.Nonempty) (h_const : ∀ j ∈ J, j ∈ I_const d ϕ U) (y : X) (hy : y ∈ ϕ.func '' U) : Fib d ϕ J y U = U := by ext x simp only [Fib, Set.mem_setOf_eq] constructor · rintro ⟨hx, _⟩; exact hx · intro hx rcases hy with ⟨x₀, hx₀, rfl⟩ refine ⟨hx, ?_⟩ dsimp [subfamily_pseudometric] apply le_antisymm _ (zero_le _) apply iSup_le rintro ⟨j, hj⟩ exact h_const j hj x hx x₀ hx₀ /-- CH03-P11-02: 命题 3.8 (i-b) 任意输入分量的点态与统一半径均为无穷 -/ theorem prop_3_8_i_b_ptwise (ϕ : Operator X bot) (U : Set X) (J : Set I) (hJ : J.Nonempty) (h_const : ∀ j ∈ J, j ∈ I_const d ϕ U) (i : I) (y : X) (hy : y ∈ U) : r_null ϕ (d i) (subfamily_pseudometric d J) y U = ⊤ := by apply le_antisymm le_top dsimp [r_null] apply le_sSup simp only [Set.mem_setOf_eq] intro b hb by_contra h_lt push_neg at h_lt obtain ⟨r, hr_lt, hr_top⟩ := ENNReal.exists_between_of_lt (show b < ⊤ from h_lt) have hr_pos : 0 < r := lt_of_le_of_lt (zero_le _) hr_lt have h_r_mem : r ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → subfamily_pseudometric d J (ϕ.func x) (ϕ.func y) = 0 } := by refine ⟨hr_pos, hr_top, ?_⟩ intro x hx _ dsimp [subfamily_pseudometric] apply le_antisymm _ (zero_le _) apply iSup_le rintro ⟨j, hj⟩ exact h_const j hj x hx y hy exact (not_le_of_gt hr_lt) (hb h_r_mem) theorem prop_3_8_i_b_uniform (ϕ : Operator X bot) (U : Set X) (J : Set I) (hJ : J.Nonempty) (h_const : ∀ j ∈ J, j ∈ I_const d ϕ U) (i : I) : r_null_uniform ϕ (d i) (subfamily_pseudometric d J) U U = ⊤ := by dsimp [r_null_uniform] apply le_antisymm le_top apply le_iInf intro y apply le_iInf intro hy rw [prop_3_8_i_b_ptwise d ϕ U J hJ h_const i y hy] /-- CH03-P11-03: 命题 3.8 (ii) 合法两点无穷输入距离反例，证明无穷统一半径不推出常值 -/ theorem prop_3_8_ii_counterexample : let U : Set TwoPt := {TwoPt.a, TwoPt.b} let d_inf : TwoIndex → TwoPt → TwoPt → ENNReal := fun idx x y => match x, y with | TwoPt.bot, TwoPt.bot => 0 | TwoPt.bot, _ => ⊤ | _, TwoPt.bot => ⊤ | TwoPt.a, TwoPt.a => 0 | TwoPt.b, TwoPt.b => 0 | TwoPt.a, TwoPt.b => match idx with | TwoIndex.i => ⊤ | TwoIndex.m => 1 | TwoPt.b, TwoPt.a => match idx with | TwoIndex.i => ⊤ | TwoIndex.m => 1 (∀ idx : TwoIndex, ExtendedPseudoMetric TwoPt TwoPt.bot (d_inf idx)) ∧ (null_matrix_entry d_inf (@operator_identity TwoPt TwoPt.bot) U TwoIndex.i TwoIndex.i = ⊤) ∧ (null_matrix_entry d_inf (@operator_identity TwoPt TwoPt.bot) U TwoIndex.m TwoIndex.i = ⊤) ∧ (TwoIndex.m ∉ I_const d_inf (@operator_identity TwoPt TwoPt.bot) U) := by intro U d_inf have h_metric : ∀ idx : TwoIndex, ExtendedPseudoMetric TwoPt TwoPt.bot (d_inf idx) := by intro idx refine { nonabsorbing := ⟨TwoPt.a, by decide⟩ dist_self := by intro x; cases x <;> rfl symm := by intro x y; cases x <;> cases y <;> (try rfl) <;> (cases idx <;> rfl) triangle := by intro x y z cases x <;> cases y <;> cases z <;> (try rfl) <;> (try decide) all_goals (cases idx <;> decide) isolate_bot := by intro x hx cases x <;> (try contradiction) <;> rfl } have h_ptwise_inf : ∀ (j : TwoIndex) (y : TwoPt), y ∈ U → r_null (@operator_identity TwoPt TwoPt.bot) (d_inf TwoIndex.i) (d_inf j) y U = ⊤ := by intro j y hy dsimp [r_null] apply le_antisymm le_top apply le_sSup intro b hb by_contra h_lt push_neg at h_lt obtain ⟨r, hr_lt, hr_top⟩ := ENNReal.exists_between_of_lt (show b < ⊤ from h_lt) have hr_pos : 0 < r := lt_of_le_of_lt (zero_le _) hr_lt have h_r_mem : r ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d_inf TwoIndex.i x y < r → d_inf j x y = 0 } := by refine ⟨hr_pos, hr_top, ?_⟩ intro x hx h_dist rcases hy with rfl | rfl <;> rcases hx with rfl | rfl · rfl · change (⊤ : ENNReal) < r at h_dist exact False.elim (not_top_lt hr_top h_dist) · change (⊤ : ENNReal) < r at h_dist exact False.elim (not_top_lt hr_top h_dist) · rfl exact (not_le_of_gt hr_lt) (hb h_r_mem) have h_unif_ii : null_matrix_entry d_inf (@operator_identity TwoPt TwoPt.bot) U TwoIndex.i TwoIndex.i = ⊤ := by dsimp [null_matrix_entry, r_null_uniform] apply le_antisymm le_top apply le_iInf intro y apply le_iInf intro hy rw [h_ptwise_inf TwoIndex.i y hy] have h_unif_mi : null_matrix_entry d_inf (@operator_identity TwoPt TwoPt.bot) U TwoIndex.m TwoIndex.i = ⊤ := by dsimp [null_matrix_entry, r_null_uniform] apply le_antisymm le_top apply le_iInf intro y apply le_iInf intro hy rw [h_ptwise_inf TwoIndex.m y hy] have h_not_const_m : TwoIndex.m ∉ I_const d_inf (@operator_identity TwoPt TwoPt.bot) U := by intro hc have hU_a : TwoPt.a ∈ U := by simp [U] have hU_b : TwoPt.b ∈ U := by simp [U] have := hc TwoPt.a hU_a TwoPt.b hU_b change (1 : ENNReal) = 0 at this revert this decide exact ⟨h_metric, h_unif_ii, h_unif_mi, h_not_const_m⟩ /-- CH03-P12-01: 命题 3.9 (i) 恒等分量的像目标纤维等于输入零距类 -/ theorem prop_3_9_i (ϕ : Operator X bot) (U : Set X) (i : I) (hi_id : i ∈ I_id d ϕ U) (hd : ExtendedPseudoMetric X bot (d i)) (y : X) : Fib d ϕ {i} (ϕ.func y) U = { x ∈ U | d i x y = 0 } := by rw [prop_3_5_vi_a d ϕ U i hi_id hd (ϕ.func y)] /-- CH03-P12-02: 命题 3.9 (ii) 有限正r0球内仅零距时，点态零化半径≥r0>0 -/ theorem prop_3_9_ii (ϕ : Operator X bot) (U : Set X) (i : I) (y : X) (hy : y ∈ U) (r₀ : ENNReal) (hr₀_pos : 0 < r₀) (hr₀_ne_top : r₀ ≠ ⊤) (h_ball : ∀ x ∈ U, d i x y < r₀ → d i x y = 0) (hi_id : i ∈ I_id d ϕ U) (hd : ExtendedPseudoMetric X bot (d i)) : r_null ϕ (d i) (d i) y U ≥ r₀ ∧ r_null ϕ (d i) (d i) y U > 0 := by have h_r_mem : r₀ ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → d i (ϕ.func x) (ϕ.func y) = 0 } := by refine ⟨hr₀_pos, lt_top_iff_ne_top.mpr hr₀_ne_top, ?_⟩ intro x hx h_dist have h_zero : d i x y = 0 := h_ball x hx h_dist rw [prop_3_1_iii d ϕ U i hi_id hd x hx y hy] exact h_zero have h_ge : r_null ϕ (d i) (d i) y U ≥ r₀ := by dsimp [r_null] exact le_sSup h_r_mem have h_pos : r_null ϕ (d i) (d i) y U > 0 := lt_of_lt_of_le hr₀_pos h_ge exact ⟨h_ge, h_pos⟩ /-- CH03-P13-01: 命题 3.10 点态子族半径等于单分量半径最小值 -/ theorem prop_3_10_ptwise_min (ϕ : Operator X bot) (U : Set X) (J : Finset I) (hJ : J.Nonempty) (i : I) (y : X) : r_null ϕ (d i) (subfamily_pseudometric d J) y U = J.inf' hJ (fun j => r_null ϕ (d i) (d j) y U) := by classical dsimp [r_null] apply le_antisymm · apply Finset.le_inf' intro j hj apply sSup_le rintro r ⟨hr_pos, hr_top, hr_ball⟩ apply le_sSup refine ⟨hr_pos, hr_top, ?_⟩ intro x hx hdist have hj_sub : d j (ϕ.func x) (ϕ.func y) ≤ subfamily_pseudometric d J (ϕ.func x) (ϕ.func y) := by dsimp [subfamily_pseudometric] exact le_iSup (fun k : {k // k ∈ (J : Set I)} => d k.1 (ϕ.func x) (ϕ.func y)) ⟨j, hj⟩ have h_zero := hr_ball x hx hdist rw [h_zero] at hj_sub exact le_antisymm hj_sub (zero_le _) · apply le_sSup intro b hb by_contra h_lt push_neg at h_lt obtain ⟨r, hr_lt, hr_top⟩ := ENNReal.exists_between_of_lt (show b < _ from h_lt) have hr_pos : 0 < r := lt_of_le_of_lt (zero_le _) (lt_of_lt_of_le hr_lt (Finset.inf'_le _ (hJ.choose_spec))) have h_r_mem : r ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → subfamily_pseudometric d J (ϕ.func x) (ϕ.func y) = 0 } := by refine ⟨hr_pos, hr_top, ?_⟩ intro x hx hdist dsimp [subfamily_pseudometric] apply le_antisymm _ (zero_le _) apply iSup_le rintro ⟨j, hj⟩ have hr_le_j : r < r_null ϕ (d i) (d j) y U := lt_of_lt_of_le hr_lt (Finset.inf'_le (fun k => r_null ϕ (d i) (d k) y U) hj) obtain ⟨r_j, hr_j_mem, hr_le_rj⟩ : ∃ r_j ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → d j (ϕ.func x) (ϕ.func y) = 0 }, r ≤ r_j := by by_contra h_none push_neg at h_none have h_bound : ∀ r_j ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → d j (ϕ.func x) (ϕ.func y) = 0 }, r_j ≤ r := by intro r_j hr_j exact le_of_not_ge (h_none r_j hr_j) have h_sSup_le : r_null ϕ (d i) (d j) y U ≤ r := sSup_le h_bound exact (not_lt_of_ge h_sSup_le) hr_le_j rcases hr_j_mem with ⟨_, _, hr_j_ball⟩ have h_dist_rj : d i x y < r_j := lt_of_lt_of_le hdist hr_le_rj exact hr_j_ball x hx h_dist_rj exact (not_le_of_gt hr_lt) (hb h_r_mem) /-- CH03-P13-02: 命题 3.10 统一半径最小值公式 -/ theorem prop_3_10_uniform_min (ϕ : Operator X bot) (U : Set X) (J : Finset I) (hJ : J.Nonempty) (i : I) : r_null_uniform ϕ (d i) (subfamily_pseudometric d J) U U = J.inf' hJ (fun j => null_matrix_entry d ϕ U j i) := by classical dsimp [r_null_uniform, null_matrix_entry] have h_pt := fun y => prop_3_10_ptwise_min d ϕ U J hJ i y simp_rw [h_pt] apply le_antisymm · apply Finset.le_inf' intro j hj apply le_iInf intro y apply le_iInf intro hy exact (iInf_le_of_le y (iInf_le_of_le hy (Finset.inf'_le (fun k => r_null ϕ (d i) (d k) y U) hj))) · apply le_iInf intro y apply le_iInf intro hy apply Finset.le_inf' intro j hj have h_le := iInf_le (fun y' => ⨅ (_ : y' ∈ U), r_null ϕ (d i) (d j) y' U) y have h_le2 := iInf_le (fun (_ : y ∈ U) => r_null ϕ (d i) (d j) y U) hy exact le_trans (Finset.inf'_le (fun k => ⨅ y' ∈ U, r_null ϕ (d i) (d k) y' U) hj) (le_trans h_le h_le2) /-- CH03-P13-03: 命题 3.10 J ⊆ K 时统一半径反单调 -/ theorem prop_3_10_antimono (ϕ : Operator X bot) (U : Set X) (J K : Finset I) (hJ : J.Nonempty) (hJK : J ⊆ K) (i : I) : r_null_uniform ϕ (d i) (subfamily_pseudometric d K) U U ≤ r_null_uniform ϕ (d i) (subfamily_pseudometric d J) U U := by classical have hK : K.Nonempty := Finset.Nonempty.mono hJK hJ rw [prop_3_10_uniform_min d ϕ U J hJ i] rw [prop_3_10_uniform_min d ϕ U K hK i] apply Finset.le_inf' intro j hj have hjK : j ∈ K := hJK hj exact Finset.inf'_le (fun k => null_matrix_entry d ϕ U k i) hjK /-- CH03-P14-01: 命题 3.11 纤维成员条件推出输出零距 -/ theorem prop_3_11_fiber_zero (ϕ : Operator X bot) (U : Set X) (j : I) (y y' : X) (hy' : y' ∈ Fib d ϕ {j} (ϕ.func y) U) (hd : ExtendedPseudoMetric X bot (d j)) : d j (ϕ.func y) (ϕ.func y') = 0 := by dsimp [Fib] at hy' rw [subfamily_pseudometric_singleton] at hy' rw [hd.symm] exact hy'.2 /-- CH03-P14-02: 命题 3.11 严格小于点态上确界时提取合法有限正半径，推出零距 -/ theorem prop_3_11_lt_sSup (ϕ : Operator X bot) (U : Set X) (i j : I) (y y' : X) (hy' : y' ∈ U) (h_lt : d i y y' < r_null ϕ (d i) (d j) y U) (hd_in : ExtendedPseudoMetric X bot (d i)) (hd_out : ExtendedPseudoMetric X bot (d j)) : d j (ϕ.func y) (ϕ.func y') = 0 := by dsimp [r_null] at h_lt obtain ⟨r, hr_mem, hr_gt⟩ : ∃ r ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → d j (ϕ.func x) (ϕ.func y) = 0 }, d i y y' < r := by by_contra h_none push_neg at h_none have h_le : sSup { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ U, d i x y < r → d j (ϕ.func x) (ϕ.func y) = 0 } ≤ d i y y' := sSup_le h_none exact (not_lt_of_ge h_le) h_lt rcases hr_mem with ⟨_, _, hr_ball⟩ rw [hd_in.symm y y'] at hr_gt have h_zero := hr_ball y' hy' hr_gt rw [hd_out.symm] exact h_zero /-- CH03-P14-03: 命题 3.11 复合输入实例 -/ theorem prop_3_11_compose_inst (ϕ₁ ϕ₂ : Operator X bot) (U₁ U₂ : Set X) (j : I) (x x' : X) (hx : x ∈ U₁) (hx' : x' ∈ U₁) (h_im : ϕ₁.func x ∈ U₂) (h_im' : ϕ₁.func x' ∈ U₂) (h_fib : ϕ₁.func x' ∈ Fib d ϕ₂ {j} (ϕ₂.func (ϕ₁.func x)) U₂) (hd : ExtendedPseudoMetric X bot (d j)) : d j ((ϕ₂ * ϕ₁).func x) ((ϕ₂ * ϕ₁).func x') = 0 := by change d j (ϕ₂.func (ϕ₁.func x)) (ϕ₂.func (ϕ₁.func x')) = 0 exact prop_3_11_fiber_zero d ϕ₂ U₂ j (ϕ₁.func x) (ϕ₁.func x') h_fib hd /-- CH03-P15-01: 命题 3.12 (i) 下游在实际像域保持零距时，复合统一半径下界 -/ theorem prop_3_12_i (ϕ₁ ϕ₂ : Operator X bot) (U : Set X) (i j l : I) (h_flow : ∀ y ∈ ϕ₁.func '' U, ∀ y' ∈ ϕ₁.func '' U, d l y y' = 0 → d j (ϕ₂.func y) (ϕ₂.func y') = 0) (hd_l : ExtendedPseudoMetric X bot (d l)) : null_matrix_entry d (ϕ₂ * ϕ₁) U j i ≥ null_matrix_entry d ϕ₁ U l i := by dsimp [null_matrix_entry, r_null_uniform] apply le_iInf intro y apply le_iInf intro hy have h_le_pt := iInf_le_of_le y (iInf_le_of_le hy (le_refl _)) refine le_trans h_le_pt ?_ dsimp [r_null] apply sSup_le rintro r ⟨hr_pos, hr_top, hr_ball⟩ apply le_sSup refine ⟨hr_pos, hr_top, ?_⟩ intro x hx h_dist have h_zero1 : d l (ϕ₁.func x) (ϕ₁.func y) = 0 := hr_ball x hx h_dist have hx_im : ϕ₁.func x ∈ ϕ₁.func '' U := Set.mem_image_of_mem _ hx have hy_im : ϕ₁.func y ∈ ϕ₁.func '' U := Set.mem_image_of_mem _ hy change d j (ϕ₂.func (ϕ₁.func x)) (ϕ₂.func (ϕ₁.func y)) = 0 exact h_flow (ϕ₁.func x) hx_im (ϕ₁.func y) hy_im h_zero1 /-- CH03-P15-02: 命题 3.12 (ii) 有限正L的单通道Lip上界给下游实际像域半径除以L的下界 -/ theorem prop_3_12_ii (ϕ₁ ϕ₂ : Operator X bot) (U : Set X) (i j l : I) (L : ENNReal) (hL_pos : 0 < L) (hL_top : L ≠ ⊤) (h_lip : ∀ x ∈ U, ∀ x' ∈ U, d l (ϕ₁.func x) (ϕ₁.func x') ≤ L * d i x x') (hd_i : ExtendedPseudoMetric X bot (d i)) (hd_l : ExtendedPseudoMetric X bot (d l)) (hd_j : ExtendedPseudoMetric X bot (d j)) : null_matrix_entry d (ϕ₂ * ϕ₁) U j i ≥ (null_matrix_entry d ϕ₂ (ϕ₁.func '' U) j l) / L := by dsimp [null_matrix_entry, r_null_uniform] by_cases h_target_zero : (⨅ y ∈ ϕ₁.func '' U, r_null ϕ₂ (d l) (d j) y (ϕ₁.func '' U)) / L = 0 · rw [h_target_zero]; exact zero_le _ apply le_iInf intro x apply le_iInf intro hx dsimp [r_null] have hx_im : ϕ₁.func x ∈ ϕ₁.func '' U := Set.mem_image_of_mem _ hx have h_pt_le : (⨅ y ∈ ϕ₁.func '' U, r_null ϕ₂ (d l) (d j) y (ϕ₁.func '' U)) ≤ r_null ϕ₂ (d l) (d j) (ϕ₁.func x) (ϕ₁.func '' U) := iInf_le_of_le (ϕ₁.func x) (iInf_le_of_le hx_im (le_refl _)) have h_div_le : (⨅ y ∈ ϕ₁.func '' U, r_null ϕ₂ (d l) (d j) y (ϕ₁.func '' U)) / L ≤ (r_null ϕ₂ (d l) (d j) (ϕ₁.func x) (ϕ₁.func '' U)) / L := by gcongr refine le_trans h_div_le ?_ apply le_sSup intro b hb by_contra h_lt push_neg at h_lt obtain ⟨r, hr_lt, hr_top⟩ := ENNReal.exists_between_of_lt (show b < _ from h_lt) have hr_pos : 0 < r := lt_of_le_of_lt (zero_le _) hr_lt have h_rL_pos : 0 < r * L := ENNReal.mul_pos (ne_of_gt hr_pos) (ne_of_gt hL_pos) have h_rL_lt : r * L < r_null ϕ₂ (d l) (d j) (ϕ₁.func x) (ϕ₁.func '' U) := by rw [← ENNReal.lt_div_iff_mul_lt (Or.inl (ne_of_gt hL_pos)) (Or.inr hL_top)] exact hr_lt have h_r_mem : r ∈ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x' ∈ U, d i x' x < r → d j ((ϕ₂ * ϕ₁).func x') ((ϕ₂ * ϕ₁).func x) = 0 } := by refine ⟨hr_pos, hr_top, ?_⟩ intro x' hx' h_dist have h_dl : d l (ϕ₁.func x') (ϕ₁.func x) < r * L := by calc d l (ϕ₁.func x') (ϕ₁.func x) ≤ L * d i x' x := h_lip x' hx' x hx _ = d i x' x * L := mul_comm _ _ _ < r * L := (ENNReal.mul_lt_mul_right (ne_of_gt hL_pos) hL_top).mpr h_dist change d j (ϕ₂.func (ϕ₁.func x')) (ϕ₂.func (ϕ₁.func x)) = 0 rw [hd_j.symm] have h_im_x' : ϕ₁.func x' ∈ ϕ₁.func '' U := Set.mem_image_of_mem _ hx' exact prop_3_11_lt_sSup d ϕ₂ (ϕ₁.func '' U) l j (ϕ₁.func x) (ϕ₁.func x') h_im_x' (by calc d l (ϕ₁.func x) (ϕ₁.func x') = d l (ϕ₁.func x') (ϕ₁.func x) := hd_l.symm _ _ _ < r * L := h_dl _ < r_null ϕ₂ (d l) (d j) (ϕ₁.func x) (ϕ₁.func '' U) := h_rL_lt) hd_l hd_j exact (not_le_of_gt hr_lt) (hb h_r_mem) /-- CH03-P18-01: 命题 3.15 (i) 严格低于统一半径的输入点对输出零距 -/ theorem prop_3_15_i (f : Operator X bot) (A U : Set X) (hAU : A ⊆ U) (i j : I) (x y : X) (hx : x ∈ A) (hy : y ∈ A) (h_dist : d i x y < r_null_uniform f (d i) (d j) A U) (hd_i : ExtendedPseudoMetric X bot (d i)) (hd_j : ExtendedPseudoMetric X bot (d j)) : d j (f.func x) (f.func y) = 0 := by have h_unif_le : r_null_uniform f (d i) (d j) A U ≤ r_null f (d i) (d j) y U := iInf_le_of_le y (iInf_le_of_le hy (le_refl _)) have h_lt : d i y x < r_null f (d i) (d j) y U := by calc d i y x = d i x y := hd_i.symm y x _ < r_null_uniform f (d i) (d j) A U := h_dist _ ≤ r_null f (d i) (d j) y U := h_unif_le have h_zero := prop_3_11_lt_sSup d f U i j y x (hAU hx) h_lt hd_i hd_j rw [hd_j.symm] exact h_zero /-- CH03-P18-02: 命题 3.15 (ii) 输出正分离推出输入距离≥统一半径 -/ theorem prop_3_15_ii (f : Operator X bot) (A U : Set X) (hAU : A ⊆ U) (i j : I) (x y : X) (hx : x ∈ A) (hy : y ∈ A) (h_out_pos : d j (f.func x) (f.func y) > 0) (hd_i : ExtendedPseudoMetric X bot (d i)) (hd_j : ExtendedPseudoMetric X bot (d j)) : d i x y ≥ r_null_uniform f (d i) (d j) A U := by by_contra h_lt push_neg at h_lt have h_zero := prop_3_15_i d f A U hAU i j x y hx hy h_lt hd_i hd_j exact (ne_of_gt h_out_pos) h_zero /-- CH03-P18-03: 命题 3.15 (iii) 零化半径不足时的分离见证 -/ theorem prop_3_15_iii (f : Operator X bot) (A : Set X) (hA : A.Nonempty) (i j : I) (τ_N α : ENNReal) (h_lt_α : r_null_uniform f (d i) (d j) A A < α) (h_α_lt : α < τ_N) (hα_top : α ≠ ⊤) : ∃ x ∈ A, ∃ y ∈ A, ∃ ε : ENNReal, 0 < ε ∧ ε < ⊤ ∧ d i x y < α ∧ ε ≤ d j (f.func x) (f.func y) := by dsimp [r_null_uniform] at h_lt_α obtain ⟨y, hy_mem, hy_lt⟩ : ∃ y ∈ A, r_null f (d i) (d j) y A < α := by by_contra h_none push_neg at h_none have h_le : α ≤ ⨅ y ∈ A, r_null f (d i) (d j) y A := le_iInf (fun y => le_iInf (fun hy => h_none y hy)) exact (not_lt_of_ge h_le) h_lt_α dsimp [r_null] at hy_lt have h_not_in : α ∉ { r : ENNReal | 0 < r ∧ r < ⊤ ∧ ∀ x ∈ A, d i x y < r → d j (f.func x) (f.func y) = 0 } := by intro h_mem have h_le := le_sSup h_mem exact (not_lt_of_ge h_le) hy_lt push_neg at h_not_in have h_haves : 0 < α ∧ α < ⊤ := ⟨lt_of_le_of_lt (zero_le _) hy_lt, lt_top_iff_ne_top.mpr hα_top⟩ have h_ball_fail := h_not_in h_haves.1 h_haves.2 rcases h_ball_fail with ⟨x, hx, h_dist, h_ne_zero⟩ have h_dist_pos : 0 < d j (f.func x) (f.func y) := lt_of_le_of_ne (zero_le _) (Ne.symm h_ne_zero) by_cases h_top : d j (f.func x) (f.func y) = ⊤ · refine ⟨x, hx, y, hy_mem, 1, by decide, by decide, h_dist, ?_⟩ rw [h_top]; exact le_top · refine ⟨x, hx, y, hy_mem, d j (f.func x) (f.func y), h_dist_pos, lt_top_iff_ne_top.mpr h_top, h_dist, le_rfl⟩ end OperatorLocalDegeneracy