Cozero.lean

1import BFPP.FSpaceNecessary2import Mathlib.Analysis.SpecificLimits.Normed3import Mathlib.Topology.Algebra.InfiniteSum.Module45/-! # Countable unions of cozero sets -/67namespace BFPP89set_option autoImplicit false1011open Set1213universe u14variable {K : Type u} [TopologicalSpace K] [CompactSpace K]1516noncomputable def normalizedAbs (f : C(K, ℝ)) : C(K, ℝ) :=17  ⟨fun t => |f t| / (1 + ‖f‖), by fun_prop⟩1819theorem normalizedAbs_bounds (f : C(K, ℝ)) (t : K) :20    0 ≤ normalizedAbs f t ∧ normalizedAbs f t ≤ 1 := by21  have hd : 0 < 1 + ‖f‖ := by linarith [norm_nonneg f]22  constructor23  · exact div_nonneg (abs_nonneg _) hd.le24  · change |f t| / (1 + ‖f‖) ≤ 125    rw [div_le_one hd]26    have h : |f t| ≤ ‖f‖ := by simpa only [Real.norm_eq_abs] using f.norm_coe_le_norm t27    linarith2829theorem normalizedAbs_norm_le (f : C(K, ℝ)) : ‖normalizedAbs f‖ ≤ 1 := by30  apply (ContinuousMap.norm_le _ (by norm_num)).mpr31  intro t32  rw [Real.norm_eq_abs, abs_of_nonneg (normalizedAbs_bounds f t).1]33  exact (normalizedAbs_bounds f t).23435@[simp] theorem normalizedAbs_eq_zero (f : C(K, ℝ)) (t : K) :36    normalizedAbs f t = 0 ↔ f t = 0 := by37  have hd : 1 + ‖f‖ ≠ 0 := ne_of_gt (by linarith [norm_nonneg f])38  change |f t| / (1 + ‖f‖) = 0 ↔ f t = 039  simp [div_eq_zero_iff, hd]4041theorem countable_union_cozero (f : ℕ → C(K, ℝ)) :42    ∃ g : C(K, ℝ), {t | g t ≠ 0} = ⋃ n, {t | f n t ≠ 0} := by43  let term : ℕ → C(K, ℝ) := fun n => (1 / 2 : ℝ) ^ n • normalizedAbs (f n)44  have hp (n : ℕ) : 0 < (1 / 2 : ℝ) ^ n := pow_pos (by norm_num) n45  have hterm (n : ℕ) : ‖term n‖ ≤ (1 / 2 : ℝ) ^ n := by46    dsimp only [term]47    rw [norm_smul, Real.norm_eq_abs, abs_of_pos (hp n)]48    simpa only [mul_one] using mul_le_mul_of_nonneg_left49      (normalizedAbs_norm_le (f n)) (hp n).le50  have hgeo : Summable (fun n : ℕ => (1 / 2 : ℝ) ^ n) :=51    summable_geometric_of_abs_lt_one (by norm_num)52  have hs : Summable term := hgeo.of_norm_bounded hterm53  let g : C(K, ℝ) := ∑' n, term n54  have hnonneg (n : ℕ) (t : K) : 0 ≤ term n t :=55    mul_nonneg (hp n).le (normalizedAbs_bounds (f n) t).156  have hzero (t : K) : g t = 0 ↔ ∀ n, f n t = 0 := by57    have hseval := (ContinuousMap.evalCLM ℝ t).summable hs58    have heval : g t = ∑' n, term n t := (ContinuousMap.evalCLM ℝ t).map_tsum hs59    constructor60    · intro hg n61      have hle : term n t ≤ ∑' k, term k t := by62        simpa only [Finset.sum_singleton] using63          hseval.sum_le_tsum {n} (fun k _hk => hnonneg k t)64      rw [← heval, hg] at hle65      have hz : term n t = 0 := le_antisymm hle (hnonneg n t)66      change (1 / 2 : ℝ) ^ n * normalizedAbs (f n) t = 0 at hz67      exact (normalizedAbs_eq_zero (f n) t).mp68        ((mul_eq_zero.mp hz).resolve_left (ne_of_gt (hp n)))69    · intro h70      rw [heval]71      have hz : ∀ n, term n t = 0 := by72        intro n73        change (1 / 2 : ℝ) ^ n * normalizedAbs (f n) t = 074        rw [(normalizedAbs_eq_zero (f n) t).mpr (h n), mul_zero]75      simp only [hz, tsum_zero]76  refine ⟨g, ?_⟩77  ext t78  simp only [Set.mem_ofPred_eq, mem_iUnion, ne_eq, hzero, not_forall]7980end BFPP

SHA-256