English
The function u defined as above is continuous.
Русский
Функция u непрерывна.
LaTeX
$$$\\text{ExistsContDiffBumpBase.u_continuous: Continuous }u$$$
Lean4
theorem u_exists :
∃ u : E → ℝ, ContDiff ℝ ∞ u ∧ (∀ x, u x ∈ Icc (0 : ℝ) 1) ∧ support u = ball 0 1 ∧ ∀ x, u (-x) = u x :=
by
have A : IsOpen (ball (0 : E) 1) := isOpen_ball
obtain ⟨f, f_support, f_smooth, f_range⟩ :
∃ f : E → ℝ, f.support = ball (0 : E) 1 ∧ ContDiff ℝ ∞ f ∧ Set.range f ⊆ Set.Icc 0 1 := A.exists_smooth_support_eq
have B : ∀ x, f x ∈ Icc (0 : ℝ) 1 := fun x => f_range (mem_range_self x)
refine ⟨fun x => (f x + f (-x)) / 2, ?_, ?_, ?_, ?_⟩
· exact (f_smooth.add (f_smooth.comp contDiff_neg)).div_const _
· intro x
simp only [mem_Icc]
constructor
· linarith [(B x).1, (B (-x)).1]
· linarith [(B x).2, (B (-x)).2]
· refine support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩
· apply ne_of_gt
have : 0 < f x := by
apply lt_of_le_of_ne (B x).1 (Ne.symm _)
rwa [← f_support] at hx
linarith [(B (-x)).1]
· have I1 : x ∉ support f := by rwa [f_support]
have I2 : -x ∉ support f := by
rw [f_support]
simpa using hx
simp only [mem_support, Classical.not_not] at I1 I2
simp only [I1, I2, add_zero, zero_div]
· intro x; simp only [add_comm, neg_neg]
