A smooth compactly supported plateau inside any open neighborhood of a compact set

Actual proof outline: Insert a compact neighborhood and obtain an auxiliary smooth function: The first two library results provide L and g with their recorded properties. Positivity on K combines nonzero support membership with nonnegativity, rather than assuming g equals one there. Choose a uniform positive lower bound on K: `exists_forall_le'` gives a strict improvement of the lower bound zero, not an extra nonempty-set premise. Compress the values through the smooth transition: This is the construction used to prove the existence theorem. The scalar transition has already been supplied by Mathlib; no new bump formula is postulated. Separate the nonzero set from the boundary of the auxiliary support: The proof weakens the strict lower bound to a non-strict one so that the containing set F is closed and can also contain the closure of the support. Control the closed support and obtain compactness: This is why using a positive superlevel threshold matters: merely knowing supp g⊆U would not by itself control its closure inside U. Verify the plateau and collect all six properties: `Set.EqOn χ 1 K` means equality on K with the constant-one function. The final nested conjunction lists exactly the six requested properties.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem exists_contDiff_eq_one_tsupport_subset
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {K U : Set E} (hK : IsCompact K) (hU : IsOpen U) (hKU : K ⊆ U) :
    ∃ χ : E → ℝ,
      Function.support χ ⊆ U ∧ tsupport χ ⊆ U ∧ HasCompactSupport χ ∧
        ContDiff ℝ (⊤ : ℕ∞) χ ∧ Set.range χ ⊆ Set.Icc 0 1 ∧ Set.EqOn χ 1 K := by
  obtain ⟨L, hL, hK_intL, hL_U⟩ := exists_compact_between hK hU hKU
  obtain ⟨g, hg_support, hg_contDiff, hg_range⟩ :=
    (isOpen_interior : IsOpen (interior L)).exists_contDiff_support_eq
      (E := E) (n := (⊤ : ℕ∞))
  have hg_pos : ∀ x ∈ K, 0 < g x := by
    intro x hx
    have hx_support : x ∈ Function.support g := by
      rw [hg_support]
      exact hK_intL hx
    exact lt_of_le_of_ne
      (hg_range (Set.mem_range_self x)).1 (Ne.symm hx_support)
  obtain ⟨m, hm_pos, hm_le⟩ :=
    hK.exists_forall_le' hg_contDiff.continuous.continuousOn hg_pos
  have hm_half_pos : 0 < m / 2 := half_pos hm_pos
  let χ : E → ℝ := fun x =>
    Real.smoothTransition ((g x - m / 2) / (m / 2))
  have hχ_support_superlevel :
      Function.support χ ⊆ {x : E | m / 2 ≤ g x} := by
    intro x hx
    change χ x ≠ 0 at hx
    have harg : 0 < (g x - m / 2) / (m / 2) := by
      apply lt_of_not_ge
      intro hnonpos
      apply hx
      exact Real.smoothTransition.zero_of_nonpos hnonpos
    have hnum : 0 < g x - m / 2 :=
      (div_pos_iff_of_pos_right hm_half_pos).mp harg
    exact (sub_pos.mp hnum).le
  have hsuperlevel_closed : IsClosed {x : E | m / 2 ≤ g x} :=
    isClosed_le continuous_const hg_contDiff.continuous
  have hχ_tsupport_superlevel :
      tsupport χ ⊆ {x : E | m / 2 ≤ g x} := by
    exact closure_minimal hχ_support_superlevel hsuperlevel_closed
  have hsuperlevel_intL : {x : E | m / 2 ≤ g x} ⊆ interior L := by
    intro x hx
    have hgx_pos : 0 < g x := hm_half_pos.trans_le hx
    have hx_support : x ∈ Function.support g := hgx_pos.ne'
    rwa [hg_support] at hx_support
  have hχ_tsupport_L : tsupport χ ⊆ L :=
    hχ_tsupport_superlevel.trans (hsuperlevel_intL.trans interior_subset)
  have hχ_tsupport_U : tsupport χ ⊆ U := hχ_tsupport_L.trans hL_U
  have hχ_support_U : Function.support χ ⊆ U :=
    (subset_tsupport χ).trans hχ_tsupport_U
  have hχ_compact : HasCompactSupport χ := by
    rw [hasCompactSupport_def]
    exact hL.of_isClosed_subset isClosed_closure hχ_tsupport_L
  have hχ_contDiff : ContDiff ℝ (⊤ : ℕ∞) χ := by
    apply Real.smoothTransition.contDiff.comp
    exact (hg_contDiff.sub contDiff_const).div_const (m / 2)
  have hχ_range : Set.range χ ⊆ Set.Icc (0 : ℝ) 1 := by
    rintro _ ⟨x, rfl⟩
    exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩
  have hχ_one : Set.EqOn χ 1 K := by
    intro x hx
    apply Real.smoothTransition.one_of_one_le
    rw [one_le_div hm_half_pos]
    linarith [hm_le x hx]
  exact ⟨χ, hχ_support_U, hχ_tsupport_U, hχ_compact,
    hχ_contDiff, hχ_range, hχ_one⟩

end Plateau

end Cutoff
end Calculus
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context