internlm/Lean-Github huggingface dataset:
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case pos
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) i = (piSplitAt i α).symm (u, x) i
Tactic:
simp
Proof state after:
no goals
Theorem: Equiv.piSplitAt_symm_zero_add_single
Proof state before:
case neg
ι : Type u_1
𝕜 : Type u_2
inst✝⁴ : NormedField 𝕜
inst✝³ : DecidableEq ι
i✝ : ι
p : ι → Prop
inst✝² : DecidablePred p
α : ι → Type u_3
inst✝¹ : (j : ι) → NormedAddCommGroup (α j)
inst✝ : (j : ι) → NormedSpace 𝕜 (α j)
i : ι
u : α i
x : (j : { j // j ≠ i }) → α ↑j
j : ι
h : ¬j = i
⊢ ((piSplitAt i α).symm (0, x) + Pi.single i u) j = (piSplitAt i α).symm (u, x) j
Tactic:
simp [h]
Proof state after:
no goals
Theorem: Subtype.fintype_subtypeEq
Proof state before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ (fintype fun x => x = i) = Fintype.subtypeEq i
Tactic:
rw [fintype, Fintype.subtypeEq]
Proof state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => x = i) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => x = i) Finset.univ ↔ a = i) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ a = i)
Theorem: Subtype.fintype_subtypeEq
Proof state before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => x = i) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => x = i) Finset.univ ↔ a = i) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ a = i)
Tactic:
simp [Finset.filter_eq']
Proof state after:
no goals
Theorem: Subtype.fintype_subtypeEq'
Proof state before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ (fintype fun x => i = x) = Fintype.subtypeEq' i
Tactic:
rw [fintype, Fintype.subtypeEq']
Proof state after:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => i = x) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => i = x) Finset.univ ↔ i = a) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ i = a)
Theorem: Subtype.fintype_subtypeEq'
Proof state before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : Fintype ι
⊢ Fintype.subtype (Finset.filter (fun x => i = x) Finset.univ)
      (_ : ∀ (a : ι), a ∈ Finset.filter (fun x => i = x) Finset.univ ↔ i = a) =
    Fintype.subtype {i} (_ : ∀ (a : ι), a ∈ {i} ↔ i = a)
Tactic:
simp [Finset.filter_eq]
Proof state after:
no goals
Theorem: MeasurableEquiv.piSplitAt_symm_apply
Proof state before:
ι : Type u_1
inst✝¹ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝ : (j : ι) → MeasurableSpace (α j)
x : α i × ((j : { j // j ≠ i }) → α ↑j)
⊢ (piSplitAt α i).symm x = (Equiv.piSplitAt i α).symm x
Tactic:
rw [piSplitAt_toEquiv]
Proof state after:
no goals
Theorem: MeasurableEquiv.measurePreserving_piSplitAt
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piSplitAt α i)
Tactic:
rw [piSplitAt_eq_trans]
Proof state after:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑((piEquivPiSubtypeProd (fun j => α j) fun j => j = i).trans
        (prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))))
Theorem: MeasurableEquiv.measurePreserving_piSplitAt
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑((piEquivPiSubtypeProd (fun j => α j) fun j => j = i).trans
        (prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))))
Tactic:
refine MeasurePreserving.trans (measurePreserving_piEquivPiSubtypeProd _ _) ?_
Proof state after:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))
Theorem: MeasurableEquiv.measurePreserving_piSplitAt
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(prodCongr (piUnique fun i_1 => α ↑i_1) (refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))
Tactic:
simp [prodCongr]
Proof state after:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑{
        toEquiv :=
          Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)),
        measurable_toFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                  (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))),
        measurable_invFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                    (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))).symm) }
Theorem: MeasurableEquiv.measurePreserving_piSplitAt
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving
    ⇑{
        toEquiv :=
          Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)),
        measurable_toFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                  (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1)))),
        measurable_invFun :=
          (_ :
            Measurable
              ⇑(Equiv.prodCongr (piUnique fun i_1 => α ↑i_1).toEquiv
                    (Equiv.refl ((i_1 : { i_1 // ¬i_1 = i }) → α ↑i_1))).symm) }
Tactic:
refine MeasurePreserving.prod ?_ (MeasurePreserving.id _)
Proof state after:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piUnique fun i_1 => α ↑i_1).toEquiv
Theorem: MeasurableEquiv.measurePreserving_piSplitAt
Proof state before:
ι : Type u_1
inst✝³ : DecidableEq ι
α : ι → Type u_2
i : ι
inst✝² : Fintype ι
inst✝¹ : (j : ι) → MeasurableSpace (α j)
μ : (j : ι) → Measure (α j)
inst✝ : ∀ (j : ι), SigmaFinite (μ j)
⊢ MeasurePreserving ⇑(piUnique fun i_1 => α ↑i_1).toEquiv
Tactic:
exact measurePreserving_piUnique _
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_const
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ HasTemperateGrowth fun x => c
Tactic:
refine ⟨contDiff_const, ?_⟩
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_const
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_const
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨0, ‖c‖, ?_⟩
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ ‖c‖ * (1 + ‖x‖) ^ 0
Theorem: Function.hasTemperateGrowth_const
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
c : F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => c) x‖ ≤ ‖c‖ * (1 + ‖x‖) ^ 0
Tactic:
cases n <;> simp [iteratedFDeriv_const_of_ne]
Proof state after:
no goals
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ Function.HasTemperateGrowth ⇑f
Tactic:
refine ⟨f.smooth', ?_⟩
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
have hf_decay := f.decay' 0 n
Proof state after:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
hf_decay : ∃ C, ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
hf_decay : ∃ C, ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases hf_decay with ⟨C, hC⟩
Proof state after:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp at hC
Proof state after:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨0, C, ?_⟩
Proof state after:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0
Theorem: SchwartzMap.hasTemperateGrowth
Proof state before:
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0
Tactic:
simpa
Proof state after:
no goals
Theorem: Finset.sum_range_choose_smul_le_pow_two_smul
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ 2 ^ n • B
Tactic:
rw [← Nat.sum_range_choose]
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ (∑ m in range (n + 1), Nat.choose n m) • B
Theorem: Finset.sum_range_choose_smul_le_pow_two_smul
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ (∑ m in range (n + 1), Nat.choose n m) • B
Tactic:
rw [Finset.sum_smul]
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ ∑ i in range (n + 1), Nat.choose n i • B
Theorem: Finset.sum_range_choose_smul_le_pow_two_smul
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), Nat.choose n i • f i ≤ ∑ i in range (n + 1), Nat.choose n i • B
Tactic:
refine Finset.sum_le_sum ?_
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∀ i ∈ range (n + 1), Nat.choose n i • f i ≤ Nat.choose n i • B
Theorem: Finset.sum_range_choose_smul_le_pow_two_smul
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∀ i ∈ range (n + 1), Nat.choose n i • f i ≤ Nat.choose n i • B
Tactic:
intro i hi
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
i : ℕ
hi : i ∈ range (n + 1)
⊢ Nat.choose n i • f i ≤ Nat.choose n i • B
Theorem: Finset.sum_range_choose_smul_le_pow_two_smul
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
R : Type u_3
inst✝¹ : OrderedAddCommMonoid R
inst✝ : OrderedSMul ℕ R
n : ℕ
f : ℕ → R
B : R
h : ∀ i ∈ range (n + 1), f i ≤ B
i : ℕ
hi : i ∈ range (n + 1)
⊢ Nat.choose n i • f i ≤ Nat.choose n i • B
Tactic:
exact smul_le_smul_of_nonneg_left (h i hi) (Nat.zero_le _)
Proof state after:
no goals
Theorem: Finset.sum_range_choose_mul_le_pow_two_mul_real
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), ↑(Nat.choose n i) * f i ≤ ↑(2 ^ n) * B
Tactic:
simp only [← nsmul_eq_mul]
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ x in range (n + 1), Nat.choose n x • f x ≤ 2 ^ n • B
Theorem: Finset.sum_range_choose_mul_le_pow_two_mul_real
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ x in range (n + 1), Nat.choose n x • f x ≤ 2 ^ n • B
Tactic:
exact Finset.sum_range_choose_smul_le_pow_two_smul h
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → E → ℝ
h : ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
induction n with
| zero => simp; use 0
| succ n h_ind =>
  specialize h_ind ?_  . intro i hi
    refine h _ ?_
    exact lt_trans hi (Nat.lt_succ_self _)
  specialize h n (Nat.lt_succ_self _)
  rcases h with ⟨k_m, C_m, hC_m⟩
  rcases h_ind with ⟨k_i, C_i, ⟨hC_i_nonneg, hC_i⟩⟩
  refine ⟨max k_i k_m, max C_i C_m, ?_⟩
  refine And.intro (le_trans hC_i_nonneg (by simp)) ?_
  intro i hi x
  simp [Nat.lt_succ] at hi
  cases lt_or_eq_of_le hi with
  | inl hi =>
    specialize hC_i i hi x
    refine le_trans hC_i ?_
    refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
  | inr hi =>
    rw [hi]
    specialize hC_m x
    refine le_trans hC_m ?_
    refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
h : ∀ i < Nat.zero, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.zero, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
simp
Proof state after:
case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
h : ∀ i < Nat.zero, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ C, 0 ≤ C
Theorem: bound_forall_range
Proof state before:
case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
h : ∀ i < Nat.zero, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ C, 0 ≤ C
Tactic:
use 0
Proof state after:
no goals
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
specialize h_ind ?_
Proof state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k

case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind :
  (∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k) → ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k

case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
. intro i hi
  refine h _ ?_
  exact lt_trans hi (Nat.lt_succ_self _)
Proof state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Theorem: bound_forall_range
Proof state before:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
specialize h n (Nat.lt_succ_self _)
Proof state after:
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∃ k C, ∀ (x : E), f n x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k