Lean4
/-- Given an open set `s` in a finite-dimensional real normed vector space, there exists a smooth
function with values in `[0, 1]` whose support is exactly `s`. -/
theorem exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
∃ f : E → ℝ, f.support = s ∧ ContDiff ℝ ∞ f ∧ Set.range f ⊆ Set.Icc 0 1 := by
/- For any given point `x` in `s`, one can construct a smooth function with support in `s` and
nonzero at `x`. By second-countability, it follows that we may cover `s` with the supports of
countably many such functions, say `g i`.
Then `∑ i, r i • g i` will be the desired function if `r i` is a sequence of positive numbers
tending quickly enough to zero. Indeed, this ensures that, for any `k ≤ i`, the `k`-th
derivative of `r i • g i` is bounded by a prescribed (summable) sequence `u i`. From this, the
summability of the series and of its successive derivatives follows. -/
rcases eq_empty_or_nonempty s with (rfl | h's)
·
exact
⟨fun _ => 0, Function.support_zero, contDiff_const, by
simp only [range_const, singleton_subset_iff, left_mem_Icc, zero_le_one]⟩
let ι := { f : E → ℝ // f.support ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
obtain ⟨T, T_count, hT⟩ : ∃ T : Set ι, T.Countable ∧ ⋃ f ∈ T, support (f : E → ℝ) = s :=
by
have : ⋃ f : ι, (f : E → ℝ).support = s :=
by
refine Subset.antisymm (iUnion_subset fun f => f.2.1) ?_
intro x hx
rcases exists_smooth_tsupport_subset (hs.mem_nhds hx) with ⟨f, hf⟩
let g : ι := ⟨f, (subset_tsupport f).trans hf.1, hf.2.1, hf.2.2.1, hf.2.2.2.1⟩
have : x ∈ support (g : E → ℝ) := by simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]
exact mem_iUnion_of_mem _ this
simp_rw [← this]
apply isOpen_iUnion_countable
rintro ⟨f, hf⟩
exact hf.2.2.1.continuous.isOpen_support
obtain ⟨g0, hg⟩ : ∃ g0 : ℕ → ι, T = range g0 :=
by
apply Countable.exists_eq_range T_count
rcases eq_empty_or_nonempty T with (rfl | hT)
· simp only [← hT, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.not_nonempty_empty] at h's
· exact hT
let g : ℕ → E → ℝ := fun n => (g0 n).1
have g_s : ∀ n, support (g n) ⊆ s := fun n => (g0 n).2.1
have s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n) := fun x hx ↦
by
rw [← hT] at hx
obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by simpa only [mem_iUnion, exists_prop] using hx
grind
have g_smooth : ∀ n, ContDiff ℝ ∞ (g n) := fun n => (g0 n).2.2.2.1
have g_comp_supp : ∀ n, HasCompactSupport (g n) := fun n => (g0 n).2.2.1
have g_nonneg : ∀ n x, 0 ≤ g n x := fun n x => ((g0 n).2.2.2.2 (mem_range_self x)).1
obtain ⟨δ, δpos, c, δc, c_lt⟩ : ∃ δ : ℕ → ℝ≥0, (∀ i : ℕ, 0 < δ i) ∧ ∃ c : NNReal, HasSum δ c ∧ c < 1 :=
NNReal.exists_pos_sum_of_countable one_ne_zero ℕ
have : ∀ n : ℕ, ∃ r : ℝ, 0 < r ∧ ∀ i ≤ n, ∀ x, ‖iteratedFDeriv ℝ i (r • g n) x‖ ≤ δ n :=
by
intro n
have : ∀ i, ∃ R, ∀ x, ‖iteratedFDeriv ℝ i (fun x => g n x) x‖ ≤ R :=
by
intro i
have : BddAbove (range fun x => ‖iteratedFDeriv ℝ i (fun x : E => g n x) x‖) :=
by
apply ((g_smooth n).continuous_iteratedFDeriv (mod_cast le_top)).norm.bddAbove_range_of_hasCompactSupport
apply HasCompactSupport.comp_left _ norm_zero
apply (g_comp_supp n).iteratedFDeriv
rcases this with ⟨R, hR⟩
exact ⟨R, fun x => hR (mem_range_self _)⟩
choose R hR using this
let M := max (((Finset.range (n + 1)).image R).max' (by simp)) 1
have δnpos : 0 < δ n := δpos n
have IR : ∀ i ≤ n, R i ≤ M := by
intro i hi
refine le_trans ?_ (le_max_left _ _)
apply Finset.le_max'
apply Finset.mem_image_of_mem
simp only [Finset.mem_range]
omega
refine ⟨M⁻¹ * δ n, by positivity, fun i hi x => ?_⟩
calc
‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ :=
by
rw [iteratedFDeriv_const_smul_apply]
exact (g_smooth n).contDiffAt.of_le (mod_cast le_top)
_ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by
rw [norm_smul _ (iteratedFDeriv ℝ i (g n) x), Real.norm_of_nonneg]; positivity
_ ≤ M⁻¹ * δ n * M := by gcongr; exact (hR i x).trans (IR i hi)
_ = δ n := by simp [field]
choose r rpos hr using this
have S : ∀ x, Summable fun n => (r n • g n) x := fun x ↦
by
refine .of_nnnorm_bounded δc.summable fun n => ?_
rw [← NNReal.coe_le_coe, coe_nnnorm]
simpa only [norm_iteratedFDeriv_zero] using hr n 0 (zero_le n) x
refine ⟨fun x => ∑' n, (r n • g n) x, ?_, ?_, ?_⟩
· apply Subset.antisymm
· intro x hx
simp only [Pi.smul_apply, Algebra.id.smul_eq_mul, mem_support, Ne] at hx
contrapose! hx
have : ∀ n, g n x = 0 := by
intro n
contrapose! hx
exact g_s n hx
simp only [this, mul_zero, tsum_zero]
· intro x hx
obtain ⟨n, hn⟩ : ∃ n, x ∈ support (g n) := s_g x hx
have I : 0 < r n * g n x := mul_pos (rpos n) (lt_of_le_of_ne (g_nonneg n x) (Ne.symm hn))
exact ne_of_gt ((S x).tsum_pos (fun i => mul_nonneg (rpos i).le (g_nonneg i x)) n I)
· refine
contDiff_tsum_of_eventually (fun n => (g_smooth n).const_smul (r n))
(fun k _ => (NNReal.hasSum_coe.2 δc).summable) ?_
intro i _
simp only [Nat.cofinite_eq_atTop, Filter.eventually_atTop]
exact ⟨i, fun n hn x => hr _ _ hn _⟩
· rintro - ⟨y, rfl⟩
refine ⟨tsum_nonneg fun n => mul_nonneg (rpos n).le (g_nonneg n y), le_trans ?_ c_lt.le⟩
have A : HasSum (fun n => (δ n : ℝ)) c := NNReal.hasSum_coe.2 δc
simp only [Pi.smul_apply, smul_eq_mul, NNReal.val_eq_coe, ← A.tsum_eq]
apply Summable.tsum_le_tsum _ (S y) A.summable
intro n
apply (le_abs_self _).trans
simpa only [norm_iteratedFDeriv_zero] using hr n 0 (zero_le n) y
