awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : (i : ℕ) → ℝ
hR :
  ∀ (i : ℕ) (x : E),
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R i
M : ℝ := max ((Finset.image R (Finset.range (n + 1))).max' ⋯) 1
δnpos : 0 < δ n
IR : ∀ i ≤ n, R i ≤ M
i : ℕ
hi : i ≤ n
x : E
ℝ :
  norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) =
    ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖
ℝ₁ :
  ‖HSMul.hSMul (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (M⁻¹ * (↑(δ n) : ℝ))
        (iteratedFDeriv ℝ i (g n) x)‖ =
    M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)
ℝ₂ :
  M⁻¹ * (↑(δ n) : ℝ) * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x) ≤
    M⁻¹ * (↑(δ n) : ℝ) * M
⊢ norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i ((M⁻¹ * (↑(δ n) : ℝ)) • g n) x) ≤
    (↑(δ n) : ℝ)
have ℝ₃ : M⁻¹ * (↑(δ n) : ℝ) * M = (↑(δ n) : ℝ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have this : ∀ (n : ℕ),
  ∃ (r : ℝ),
    0 < r ∧
      ∀ i ≤ n,
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤ (↑(δ n) : ℝ)
Tactic: 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]
      lia
    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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
this :
  ∀ (n : ℕ),
    ∃ (r : ℝ),
      0 < r ∧
        ∀ i ≤ n,
          ∀ (x : E),
            norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r • g n) x) ≤
              (↑(δ n) : ℝ)
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have inr : ∀ (r : (n : ℕ) → ℝ) (rpos : ∀ (n : ℕ), 0 < r n)
  (hr :
    ∀ (n i : ℕ),
      i ≤ n →
        ∀ (x : E),
          norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤
            (↑(δ n) : ℝ)),
  ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
Tactic: choose r rpos hr using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
x : E
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
have refine : ∀ (n : ℕ), ‖(r n • g n) x‖₊ ≤ δ n
Tactic: refine .of_nnnorm_bounded δc.summable fun n => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
Tactic: 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 x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have inr : (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) = s
Tactic: refine ⟨fun x => ∑' n, (r n • g n) x, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
inr : (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) = s
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have inr₁ : ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
Tactic: refine ⟨fun x => ∑' n, (r n • g n) x, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
inr : (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) = s
inr₁ : ContDiff ℝ (F := ℝ) (↑n : ℕ∞ω) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
have inr₂ : Subset (α := Set ℝ) (range fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) (Icc 0 1)
Tactic: refine ⟨fun x => ∑' n, (r n • g n) x, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
⊢ (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) = s
have inr : (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) ⊆ s
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
inr : (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) ⊆ s
⊢ (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) = s
have inr₁ : s ⊆ support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : Membership.mem (γ := Set E) (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) x
⊢ x ∈ s
have hx₁ : ¬Eq (α := ℝ) (∑' (n : ℕ), r n * g n x) 0
Tactic: simp only [Pi.smul_apply, smul_eq_mul, mem_support, Ne] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : ¬Eq (α := ℝ) (∑' (n : ℕ), r n * g n x) 0
⊢ x ∈ s
have inr : ∀ (hx : x ∉ s), Eq (α := ℝ) (∑' (n : ℕ), r n * g n x) 0
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : x ∉ s
n : ℕ
⊢ g n x = 0
have contrapose! : ∀ (hx : g n x ≠ 0), x ∈ s
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : x ∉ s
⊢ Eq (α := ℝ) (∑' (n : ℕ), r n * g n x) 0
have this : ∀ (n : ℕ), g n x = 0
Tactic: have : ∀ n, g n x = 0 := by
        intro n
        contrapose! hx
        exact g_s n hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E) (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) x
have inr : ∀ (n : ℕ) (hn : x ∈ support (g n)),
  Membership.mem (γ := Set E) (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) x
Tactic: obtain ⟨n, hn⟩ : ∃ n, x ∈ support (g n) := s_g x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
x : E
hx : x ∈ s
n : ℕ
hn : x ∈ support (g n)
⊢ Membership.mem (γ := Set E) (support (M := ℝ) fun (x : E) ↦ ∑' (n : ℕ), (r n • g n) x) x
have I : 0 < r n * g n x
Tactic: have I : 0 < r n * g n x := mul_pos (rpos n) (lt_of_le_of_ne (g_nonneg n x) (Ne.symm hn))