internlm/Lean-Github huggingface dataset:
Theorem: integral_piSplitAt_right
Proof state before:
case hf
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
hf : Integrable f
⊢ Integrable (Function.uncurry fun u x => f ((Equiv.piSplitAt i fun i => D i).symm (u, x)))
Tactic:
rw [Function.uncurry_def]
Proof state after:
case hf
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
hf : Integrable f
⊢ Integrable fun p => f ((Equiv.piSplitAt i fun i => D i).symm (p.1, p.2))
Theorem: integral_piSplitAt_right
Proof state before:
case hf
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : ((i : ι) → D i) → F
hf : Integrable f
⊢ Integrable fun p => f ((Equiv.piSplitAt i fun i => D i).symm (p.1, p.2))
Tactic:
exact hf.piSplitAt i
Proof state after:
no goals
Theorem: integral_funSplitAt_right
Proof state before:
ι : Type u_1
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
mE : MeasureSpace E
inst✝⁶ : SigmaFinite volume
D : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁴ : (i : ι) → NormedSpace ℝ (D i)
mD : (i : ι) → MeasureSpace (D i)
inst✝³ : ∀ (i : ι), SigmaFinite volume
F : Type u_4
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
i : ι
f : (ι → E) → F
hf : Integrable f
⊢ ∫ (x : ι → E), f x = ∫ (x : { j // j ≠ i } → E) (u : E), f ((Equiv.funSplitAt i E).symm (u, x))
Tactic:
exact integral_piSplitAt_right i hf
Proof state after:
no goals
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (fun u => f (Function.update x i u)) (f' (Pi.single i 1)) (x i)
Tactic:
change HasDerivAt (f ∘ Function.update x i) _ _
Proof state after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
have : HasFDerivAt (f ∘ Function.update x i) (f'.comp (.pi (Pi.single i (.id 𝕜 𝕜)))) (x i)
Proof state after:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)

ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)

ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
. refine HasFDerivAt.comp _ (by simpa using hf) (hasFDerivAt_update x _)
Proof state after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
refine HasDerivAt.congr_deriv this.hasDerivAt ?_
Proof state after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) 1 =
    f' (Pi.single i 1)
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) 1 =
    f' (Pi.single i 1)
Tactic:
simp
Proof state after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (f' fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = f' (Pi.single i 1)
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (f' fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = f' (Pi.single i 1)
Tactic:
refine congrArg _ ?_
Proof state after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = Pi.single i 1
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = Pi.single i 1
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case h
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
by_cases h : j = i
Proof state after:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
. rw [h]; simp
Proof state after:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
. simp [h]
Proof state after:
no goals
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
Tactic:
refine HasFDerivAt.comp _ (by simpa using hf) (hasFDerivAt_update x _)
Proof state after:
no goals
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt f f' (Function.update x i (x i))
Tactic:
simpa using hf
Proof state after:
no goals
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
rw [h]
Proof state after:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i) 1 = Pi.single i 1 i
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i) 1 = Pi.single i 1 i
Tactic:
simp
Proof state after:
no goals
Theorem: HasFDerivAt.hasDerivAt_comp_update
Proof state before:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
simp [h]
Proof state after:
no goals
Theorem: IsBump.mul
Proof state before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ IsBump (f * g)
Tactic:
simp [IsBump]
Proof state after:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g) ∧ ContDiff ℝ ⊤ (f * g)
Theorem: IsBump.mul
Proof state before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g) ∧ ContDiff ℝ ⊤ (f * g)
Tactic:
apply And.intro
Proof state after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Theorem: IsBump.mul
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
. apply HasCompactSupport.mul_right hf.left
Proof state after:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Theorem: IsBump.mul
Proof state before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
. exact ContDiff.mul hf.right hg.right
Proof state after:
no goals
Theorem: IsBump.mul
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)
Tactic:
apply HasCompactSupport.mul_right hf.left
Proof state after:
no goals
Theorem: IsBump.mul
Proof state before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
exact ContDiff.mul hf.right hg.right
Proof state after:
no goals
Theorem: IsBump.differentiable
Proof state before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ 1 ≤ ⊤
Tactic:
norm_num
Proof state after:
no goals
Theorem: IsBump.comp_neg
Proof state before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ IsBump fun x => f (-x)
Tactic:
constructor
Proof state after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Theorem: IsBump.comp_neg
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
. have h_neg {x : α} : -x = (Homeomorph.neg α) x := by simp [Homeomorph.neg]
  simp_rw [h_neg]
  exact HasCompactSupport.comp_homeomorph hf.left _
Proof state after:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Theorem: IsBump.comp_neg
Proof state before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
. exact ContDiff.comp hf.right contDiff_neg
Proof state after:
no goals
Theorem: IsBump.comp_neg
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)
Tactic:
have h_neg {x : α} : -x = (Homeomorph.neg α) x := by simp [Homeomorph.neg]
Proof state after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f (-x)
Theorem: IsBump.comp_neg
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f (-x)
Tactic:
simp_rw [h_neg]
Proof state after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f ((Homeomorph.neg α) x)
Theorem: IsBump.comp_neg
Proof state before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f ((Homeomorph.neg α) x)
Tactic:
exact HasCompactSupport.comp_homeomorph hf.left _
Proof state after:
no goals
Theorem: IsBump.comp_neg
Proof state before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
x : α
⊢ -x = (Homeomorph.neg α) x
Tactic:
simp [Homeomorph.neg]
Proof state after:
no goals
Theorem: IsBump.comp_neg
Proof state before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
exact ContDiff.comp hf.right contDiff_neg
Proof state after:
no goals
Theorem: IsBump.integrable
Proof state before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable f
Tactic:
apply Continuous.integrable_of_hasCompactSupport
Proof state after:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f