internlm/Lean-Github huggingface dataset:
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ici δ)
Tactic:
simp
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
Proof state after:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 ≤ᵐ[volume] fun a => DiracSeq (↑↑n) a
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 ≤ᵐ[volume] fun a => DiracSeq (↑↑n) a
Tactic:
exact Filter.eventually_of_forall DiracSeq.nonneg_nat
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hI₂ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Ioi a, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
Proof state after:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
Proof state after:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
clear hδε hε ε
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp [integral_union, hδ.le, h_integrable.integrableOn]
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds 0)
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds 0)
Tactic:
conv => rhs; rw [← add_zero 0]
Proof state after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds (0 + 0))
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds (0 + 0))
Tactic:
exact Tendsto.add (hI₁ hδ) (hI₂ hδ)
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
Proof state after:
no goals
Theorem: tendsto_integral_bump_mul_deltaSeq
Proof state before:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
Proof state after:
no goals
Theorem: fderiv_const_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ fderiv ℝ (fun x => innerSL ℝ) x = 0
Tactic:
rw [fderiv_const]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ 0 x = 0
Theorem: fderiv_const_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ 0 x = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ fderiv ℝ (fun x => (innerSL ℝ) x) x = innerSL ℝ
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ∀ (x_1 : E), (fderiv ℝ (fun x => (innerSL ℝ) x) x) x_1 = (innerSL ℝ) x_1
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ∀ (x_1 : E), (fderiv ℝ (fun x => (innerSL ℝ) x) x) x_1 = (innerSL ℝ) x_1
Tactic:
intro u
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ (fderiv ℝ (fun x => (innerSL ℝ) x) x) u = (innerSL ℝ) u
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ (fderiv ℝ (fun x => (innerSL ℝ) x) x) u = (innerSL ℝ) u
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ ∀ (x_1 : E), ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) x_1 = ((innerSL ℝ) u) x_1
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ ∀ (x_1 : E), ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) x_1 = ((innerSL ℝ) u) x_1
Tactic:
intro dx
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) dx = ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) dx = ((innerSL ℝ) u) dx
Tactic:
rw [fderiv_clm_apply (differentiableAt_const _) differentiableAt_id']
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x) +
          (ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x)
        u)
      dx =
    ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x) +
          (ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x)
        u)
      dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.add_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u +
        ((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u)
      dx =
    ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u +
        ((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u)
      dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.add_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u) dx =
    ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u) dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.flip_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((fderiv ℝ (fun x => innerSL ℝ) x) u) x) dx =
    ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((fderiv ℝ (fun x => innerSL ℝ) x) u) x) dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [fderiv_const]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + (((0 x) u) x) dx = ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + (((0 x) u) x) dx = ((innerSL ℝ) u) dx
Tactic:
change _ + 0 = _
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + 0 = ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + 0 = ((innerSL ℝ) u) dx
Tactic:
simp
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (ContinuousLinearMap.id ℝ E)) u) dx = ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (ContinuousLinearMap.id ℝ E)) u) dx = ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.comp_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((innerSL ℝ) ((ContinuousLinearMap.id ℝ E) u)) dx = ((innerSL ℝ) u) dx
Theorem: fderiv_innerSL_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((innerSL ℝ) ((ContinuousLinearMap.id ℝ E) u)) dx = ((innerSL ℝ) u) dx
Tactic:
rfl
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ HasTemperateGrowth fun x => (innerSL ℝ) x
Tactic:
refine ⟨contDiff_const.clm_apply contDiff_id, ?_⟩
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨1, 1, ?_⟩
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1