awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
s : Finset (Fin n)
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
          (p (n - s.card + s.card)) *
        r ^ s.card *
      r' ^ (n - s.card) =
    ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
have h : ‖p n‖₊ * r ^ s.card * r' ^ (n - s.card) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
Tactic: rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
s : Finset (Fin n)
h : ‖p n‖₊ * r ^ s.card * r' ^ (n - s.card) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
          (p (n - s.card + s.card)) *
        r ^ s.card *
      r' ^ (n - s.card) =
    ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
have h₁ : ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
Tactic: rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
⊢ HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)
have convert_2 : HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)))
  (‖p n‖₊ * ∑ s : Finset (Fin n), r ^ s.card * r' ^ (n - s.card))
Tactic: rw [← Fin.sum_pow_mul_eq_add_pow]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ≥0) fun (x : (n : ℕ) × Finset (Fin n)) ↦
    nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                      x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) ↦
              E)
            F)
          (p
            (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
              x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) *
        r ^ x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card *
      r' ^ (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
have this : ∀ (n : ℕ),
  HasSum
    (fun (s : Finset (Fin n)) ↦
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
            (p (n - s.card + s.card)) *
          r ^ s.card *
        r' ^ (n - s.card))
    (‖p n‖₊ * (r + r') ^ n)
Tactic: have : ∀ n : ℕ,
      HasSum (fun s : Finset (Fin n) => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card))
        (‖p n‖₊ * (r + r') ^ n) := by
    intro n
    -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails?
    convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
    · ext1 s
      rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
    rw [← Fin.sum_pow_mul_eq_add_pow]
    exact (hasSum_fintype _).mul_left _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
⊢ Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      r ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
have rcases : ∀ (r' : ℝ≥0) (h0 : 0 < r') (hr' : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius),
  Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      r ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
Tactic: rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
⊢ Summable (α := ℝ≥0) fun (l : ℕ) ↦ ‖p.changeOriginSeries k l‖₊ * r ^ l
have refine : ∀ (n : ℕ),
  ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    ∑' (y : { s : Finset (Fin (k + n)) // s.card = n }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (k +
                      Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) *
        r ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y)
Tactic: refine NNReal.summable_of_le
    (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    ∑' (y : { s : Finset (Fin (k + n)) // s.card = n }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (k +
                      Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) *
        r ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y)
have simp : ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
  (∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))) *
    r ^ n
Tactic: simp only [NNReal.tsum_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k n : ℕ
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    (∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))) *
      r ^ n
have bc : ‖p.changeOriginSeries k n‖₊ ≤
  ∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
    nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ ‖p.changeOrigin x k‖₊ ≤
    ∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
          (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
have refine : HasSum (α := ℝ≥0)
  (fun (l : ℕ) ↦
    ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l)
  (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))
Tactic: refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ HasSum (α := ℝ≥0)
    (fun (l : ℕ) ↦
      ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) *
          ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
          (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))
have this : Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
  nnnorm (E :=
      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
        (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
      (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
    ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
Tactic: have := p.changeOriginSeries_summable_aux₂ h k
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
⊢ HasSum (α := ℝ≥0)
    (fun (l : ℕ) ↦
      ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) *
          ‖x‖₊ ^ l)
    (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
          (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))
have refine : ∀ (l : ℕ),
  HasSum (α := ℝ≥0)
    (fun (c : { s : Finset (Fin (k + l)) // s.card = l }) ↦
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (k +
                      Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) *
        ‖x‖₊ ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))
    (∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l)
Tactic: refine HasSum.sigma this.hasSum fun l => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
⊢ p.radius - (↑‖x‖₊ : ℝ≥0∞) ≤ (p.changeOrigin x).radius
have refine : ∀ (r : ℝ≥0) (_h0 : 0 < r) (hr : (↑r : ℝ≥0∞) < p.radius - (↑‖x‖₊ : ℝ≥0∞)), (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius
Tactic: refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑r : ℝ≥0∞) < p.radius - (↑‖x‖₊ : ℝ≥0∞)
⊢ (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius
have hr₁ : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
Tactic: rw [lt_tsub_iff_right, add_comm] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius
have hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
Tactic: have hr' : (‖x‖₊ : ℝ≥0∞) < p.radius := (le_add_right le_rfl).trans_lt hr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius
have h : Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n
Tactic: apply le_radius_of_summable_nnnorm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
k : ℕ
⊢ ‖p.changeOrigin x k‖₊ * r ^ k ≤
    (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E :=
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
              (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
            (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
          ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
      r ^ k
have bc : ‖p.changeOrigin x k‖₊ ≤
  ∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n
have this : ∀ (k : ℕ),
  ‖p.changeOrigin x k‖₊ * r ^ k ≤
    (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E :=
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
              (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
            (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
          ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
      r ^ k
Tactic: have (k : ℕ) :
      ‖p.changeOrigin x k‖₊ * r ^ k ≤
        (∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1) *
          r ^ k := by
    gcongr; exact p.nnnorm_changeOrigin_le k hr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤
      (∑' (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }),
          nnnorm (E :=
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
                (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
              (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
            ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
        r ^ k
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n
have h : Summable (α := ℝ≥0) fun (b : ℕ) ↦
  (∑' (s : (l : ℕ) × { s : Finset (Fin (b + l)) // s.card = l }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun (i : Fin (b + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l }))) ↦ E) F)
          (p (b + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l })) *
    r ^ b
Tactic: refine NNReal.summable_of_le this ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ p.radius ≤ p.derivSeries.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
have apply : ∀ (n : ℕ),
  ‖p.derivSeries n‖ ≤
    norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
      (p.changeOriginSeries 1 n)
Tactic: apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ ‖p.derivSeries n‖ ≤
    norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
      (p.changeOriginSeries 1 n)
have apply : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F)
      (↑(↑(continuousMultilinearCurryFin1 𝕜 E F) : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F ≃L[𝕜] E →L[𝕜] F) :
        ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F) *
    norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
      (p.changeOriginSeries 1 n) ≤
  norm (E :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
    (p.changeOriginSeries 1 n)
Tactic: apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans