internlm/Lean-Github huggingface dataset:
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ (fun i de dx => dx + (revDerivProj R Unit (fun x => ‖f x‖₂[R]) x).2 i de) = fun x_1 dr dx =>
    (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Tactic:
fun_trans (disch:=assumption) only
Proof state after:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ (fun i de dx =>
      dx +
        (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * de) •
          (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr dx => (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule
Proof state before:
case h
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
x : X
⊢ (fun i de dx =>
      dx +
        (‖(revDeriv R (fun x => f x) x).1‖₂[R]⁻¹ * de) •
          (revDeriv R (fun x => f x) x).2 (revDeriv R (fun x => f x) x).1) =
    fun x_1 dr dx => (revDerivUpdate R f x).2 ((‖f x‖₂[R]⁻¹ * dr) • f x) dx
Tactic:
simp[revDeriv,revDerivUpdate,smul_pull]
Proof state after:
no goals
Theorem: SciLean.norm₂.arg_x.revDerivProjUpdate_rule
Proof state before:
case funProp.discharger
K : Type
inst✝³⁰ : RCLike K
X✝ : Type
inst✝²⁹ : SemiInnerProductSpace K X✝
Y✝ : Type
inst✝²⁸ : SemiInnerProductSpace K Y✝
Z : Type
inst✝²⁷ : SemiInnerProductSpace K Z
X' Xi : Type
XI : Xi → Type
inst✝²⁶ : StructType X' Xi XI
inst✝²⁵ : IndexType Xi
inst✝²⁴ : LawfulIndexType Xi
inst✝²³ : DecidableEq Xi
Y' Yi : Type
YI : Yi → Type
inst✝²² : StructType Y' Yi YI
inst✝²¹ : IndexType Yi
inst✝²⁰ : LawfulIndexType Yi
inst✝¹⁹ : DecidableEq Yi
Z' Zi : Type
ZI : Zi → Type
inst✝¹⁸ : StructType Z' Zi ZI
inst✝¹⁷ : IndexType Zi
inst✝¹⁶ : LawfulIndexType Zi
inst✝¹⁵ : DecidableEq Zi
inst✝¹⁴ : SemiInnerProductSpace K X'
inst✝¹³ : (i : Xi) → SemiInnerProductSpace K (XI i)
inst✝¹² : SemiInnerProductSpaceStruct K X' Xi XI
inst✝¹¹ : SemiInnerProductSpace K Y'
inst✝¹⁰ : (i : Yi) → SemiInnerProductSpace K (YI i)
inst✝⁹ : SemiInnerProductSpaceStruct K Y' Yi YI
inst✝⁸ : SemiInnerProductSpace K Z'
inst✝⁷ : (i : Zi) → SemiInnerProductSpace K (ZI i)
inst✝⁶ : SemiInnerProductSpaceStruct K Z' Zi ZI
W : Type
inst✝⁵ : SemiInnerProductSpace K W
ι : Type
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : SemiInnerProductSpace R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
hf : HasAdjDiff R f
hx : ∀ (x : X), f x ≠ 0
x : X
i : Unit
de : R
dx : X
⊢ ∀ (x : X), f x ≠ 0
Tactic:
assumption
Proof state after:
no goals
Theorem: SciLean.Distribution.ext
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.28587
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type u_3
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.30196
inst✝² : Vec R Z
U : Type ?u.30217
inst✝¹ : Vec R U
V : Type ?u.30238
inst✝ : Vec R V
x y : 𝒟'(X, Y)
⊢ (∀ (φ : 𝒟 X), x φ = y φ) → x = y
Tactic:
apply SmoothLinearMap.ext
Proof state after:
no goals
Theorem: SciLean.action_dirac
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.108595
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type ?u.109415
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.110204
inst✝² : Vec R Z
U : Type ?u.110225
inst✝¹ : Vec R U
V : Type ?u.110246
inst✝ : Vec R V
x : X
φ : 𝒟 X
⊢ (dirac x) φ = φ x
Tactic:
simp[dirac]
Proof state after:
no goals
Theorem: SciLean.action_bind
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type u_4
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.114701
inst✝² : Vec R Z
U : Type u_3
inst✝¹ : Vec R U
V : Type u_5
inst✝ : Vec R V
x : 𝒟'(X, U)
f : X → 𝒟'(Y, V)
L : U ⊸[R] V ⊸[R] W
φ : 𝒟 Y
⊢ (Distribution.bind x f L) φ = x.extAction (fun x' => Distribution.extAction' (f x') ⇑φ) L
Tactic:
simp[Distribution.bind]
Proof state after:
no goals
Theorem: SciLean.Distribution.zero_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_3
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_5
inst✝⁵ : Vec R X
Y : Type ?u.121132
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.121921
inst✝² : Vec R Z
U : Type u_2
inst✝¹ : Vec R U
V : Type u_4
inst✝ : Vec R V
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪0, φ⟫[L] = 0
Tactic:
unfold extAction
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_3
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_5
inst✝⁵ : Vec R X
Y : Type ?u.121132
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.121921
inst✝² : Vec R Z
U : Type u_2
inst✝¹ : Vec R U
V : Type u_4
inst✝ : Vec R V
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ (if h : ∃ zₙ φₙ, ∀ (x : X), ∑' (i : ℕ), (φₙ i) x • zₙ i = φ x then
      let zₙ := choose h;
      let φₙ := Exists.choose ⋯;
      ∑' (i : ℕ), (L (0 (φₙ i))) (zₙ i)
    else 0) =
    0
Theorem: SciLean.Distribution.zero_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_3
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_5
inst✝⁵ : Vec R X
Y : Type ?u.121132
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.121921
inst✝² : Vec R Z
U : Type u_2
inst✝¹ : Vec R U
V : Type u_4
inst✝ : Vec R V
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ (if h : ∃ zₙ φₙ, ∀ (x : X), ∑' (i : ℕ), (φₙ i) x • zₙ i = φ x then
      let zₙ := choose h;
      let φₙ := Exists.choose ⋯;
      ∑' (i : ℕ), (L (0 (φₙ i))) (zₙ i)
    else 0) =
    0
Tactic:
simp
Proof state after:
no goals
Theorem: SciLean.Distribution.add_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_4
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type ?u.151418
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.152207
inst✝² : Vec R Z
U : Type u_3
inst✝¹ : Vec R U
V : Type u_5
inst✝ : Vec R V
T T' : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪T + T', φ⟫[L] = ⟪T, φ⟫[L] + ⟪T', φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.sub_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_4
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type ?u.157293
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.158082
inst✝² : Vec R Z
U : Type u_3
inst✝¹ : Vec R U
V : Type u_5
inst✝ : Vec R V
T T' : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪T - T', φ⟫[L] = ⟪T, φ⟫[L] - ⟪T', φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.smul_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_4
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type ?u.161826
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.162615
inst✝² : Vec R Z
U : Type u_3
inst✝¹ : Vec R U
V : Type u_5
inst✝ : Vec R V
r : R
T : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪r • T, φ⟫[L] = r • ⟪T, φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.neg_extAction
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_4
inst✝⁷ : Vec R W
inst✝⁶ : Module ℝ W
X : Type u_2
inst✝⁵ : Vec R X
Y : Type ?u.166450
inst✝⁴ : Vec R Y
inst✝³ : Module ℝ Y
Z : Type ?u.167239
inst✝² : Vec R Z
U : Type u_3
inst✝¹ : Vec R U
V : Type u_5
inst✝ : Vec R V
T : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪-T, φ⟫[L] = -⟪T, φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.fintype_sum_extAction
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type u_5
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_3
inst✝⁶ : Vec R X
Y : Type ?u.169667
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.170456
inst✝³ : Vec R Z
U : Type u_4
inst✝² : Vec R U
V : Type u_6
inst✝¹ : Vec R V
I : Type u_1
inst✝ : Fintype I
T : I → 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪∑ i : I, T i, φ⟫[L] = ∑ i : I, ⟪T i, φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.indextype_sum_extAction
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type (max (max u_2 u_3) u_4)
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_3
inst✝⁶ : Vec R X
Y : Type ?u.174847
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.175636
inst✝³ : Vec R Z
U : Type u_4
inst✝² : Vec R U
V : Type u_5
inst✝¹ : Vec R V
I : Type u_1
inst✝ : IndexType I
T : I → 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪ ∑ i, T i, φ⟫[L] = ∑ i, ⟪T i, φ⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.action_iteD
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type ?u.198948
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_1
inst✝⁶ : Vec R X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.200557
inst✝³ : Vec R Z
U : Type ?u.200578
inst✝² : Vec R U
V : Type ?u.200599
inst✝¹ : Vec R V
inst✝ : MeasureSpace X
A : Set X
t e : 𝒟'(X, Y)
φ : 𝒟 X
⊢ (ifD A then
        t
      else
        e)
      φ =
    ⟪t, fun x => if x ∈ A then φ x else 0⟫[fun y ⊸[R] fun r ⊸[R] r • y] +
      ⟪e, fun x => if x ∉ A then φ x else 0⟫[fun y ⊸[R] fun r ⊸[R] r • y]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.iteD_same
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type ?u.208374
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_1
inst✝⁶ : Vec R X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.209983
inst✝³ : Vec R Z
U : Type ?u.210004
inst✝² : Vec R U
V : Type ?u.210025
inst✝¹ : Vec R V
inst✝ : MeasureSpace X
A : Set X
u : 𝒟'(X, Y)
⊢ (ifD A then
      u
    else
      u) =
    u
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.extAction_iteD
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_1
inst✝⁶ : Vec R X
Y : Type ?u.211766
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.212555
inst✝³ : Vec R Z
U : Type u_3
inst✝² : Vec R U
V : Type u_5
inst✝¹ : Vec R V
inst✝ : MeasureSpace X
A : Set X
t e : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪ifD A then
        t
      else
        e,
      φ⟫[L] =
    ⟪t, fun x => if x ∈ A then φ x else 0⟫[L] + ⟪e, fun x => if x ∉ A then φ x else 0⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.iteD_restrict
Proof state before:
R : Type u_1
inst✝⁹ : RealScalar R
W : Type ?u.265893
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_2
inst✝⁶ : Vec R X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.267502
inst✝³ : Vec R Z
U : Type ?u.267523
inst✝² : Vec R U
V : Type ?u.267544
inst✝¹ : Vec R V
inst✝ : MeasureSpace X
T : 𝒟'(X, Y)
A : Set X
⊢ (ifD A then
      T
    else
      0) =
    T.restrict A
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Distribution.extAction_iteD'
Proof state before:
R : Type u_2
inst✝⁹ : RealScalar R
W : Type u_4
inst✝⁸ : Vec R W
inst✝⁷ : Module ℝ W
X : Type u_1
inst✝⁶ : Vec R X
Y : Type ?u.272070
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.272859
inst✝³ : Vec R Z
U : Type u_3
inst✝² : Vec R U
V : Type u_5
inst✝¹ : Vec R V
inst✝ : MeasureSpace X
A B : Set X
t e : 𝒟'(X, U)
φ : X → V
L : U ⊸[R] V ⊸[R] W
⊢ ⟪(ifD A then
            t
          else
            e).restrict
        B,
      φ⟫[L] =
    ⟪t.restrict B, fun x => if x ∈ A then φ x else 0⟫[L] + ⟪e.restrict B, fun x => if x ∉ A then φ x else 0⟫[L]
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Distribution.postComp.arg_T.IsSmoothLinarMap_rule
Proof state before:
R : Type u_1
inst✝¹³ : RealScalar R
W : Type u_5
inst✝¹² : Vec R W
inst✝¹¹ : Module ℝ W
X : Type u_2
inst✝¹⁰ : Vec R X
Y : Type u_3
inst✝⁹ : Vec R Y
inst✝⁸ : Module ℝ Y
Z : Type u_4
inst✝⁷ : Vec R Z
U : Type ?u.301798
inst✝⁶ : Vec R U
V : Type ?u.301819
inst✝⁵ : Vec R V
inst✝⁴ : MeasureSpace X
X₁ : Type ?u.301843
inst✝³ : Vec R X₁
X₂ : Type ?u.301864
inst✝² : Vec R X₂
Y₁ : Type ?u.301885
inst✝¹ : Vec R Y₁
Y₂ : Type ?u.301906
inst✝ : Vec R Y₂
T : W → 𝒟'(X, Y)
f : Y ⊸[R] Z
hT : IsSmoothLinearMap R T
⊢ IsSmoothLinearMap R fun w => postComp (T w) f
Tactic:
unfold postComp
Proof state after:
R : Type u_1
inst✝¹³ : RealScalar R
W : Type u_5
inst✝¹² : Vec R W
inst✝¹¹ : Module ℝ W
X : Type u_2
inst✝¹⁰ : Vec R X
Y : Type u_3
inst✝⁹ : Vec R Y
inst✝⁸ : Module ℝ Y
Z : Type u_4
inst✝⁷ : Vec R Z
U : Type ?u.301798
inst✝⁶ : Vec R U
V : Type ?u.301819
inst✝⁵ : Vec R V
inst✝⁴ : MeasureSpace X
X₁ : Type ?u.301843
inst✝³ : Vec R X₁
X₂ : Type ?u.301864
inst✝² : Vec R X₂
Y₁ : Type ?u.301885
inst✝¹ : Vec R Y₁
Y₂ : Type ?u.301906
inst✝ : Vec R Y₂
T : W → 𝒟'(X, Y)
f : Y ⊸[R] Z
hT : IsSmoothLinearMap R T
⊢ IsSmoothLinearMap R fun w => fun φ ⊸[R] f ((T w) φ)
Theorem: SciLean.Distribution.postComp.arg_T.IsSmoothLinarMap_rule
Proof state before:
R : Type u_1
inst✝¹³ : RealScalar R
W : Type u_5
inst✝¹² : Vec R W
inst✝¹¹ : Module ℝ W
X : Type u_2
inst✝¹⁰ : Vec R X
Y : Type u_3
inst✝⁹ : Vec R Y
inst✝⁸ : Module ℝ Y
Z : Type u_4
inst✝⁷ : Vec R Z
U : Type ?u.301798
inst✝⁶ : Vec R U
V : Type ?u.301819
inst✝⁵ : Vec R V
inst✝⁴ : MeasureSpace X
X₁ : Type ?u.301843
inst✝³ : Vec R X₁
X₂ : Type ?u.301864
inst✝² : Vec R X₂
Y₁ : Type ?u.301885
inst✝¹ : Vec R Y₁
Y₂ : Type ?u.301906
inst✝ : Vec R Y₂
T : W → 𝒟'(X, Y)
f : Y ⊸[R] Z
hT : IsSmoothLinearMap R T
⊢ IsSmoothLinearMap R fun w => fun φ ⊸[R] f ((T w) φ)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Function.toDistribution_action
Proof state before:
R : Type u_1
inst✝¹³ : RealScalar R
W : Type ?u.338194
inst✝¹² : Vec R W
inst✝¹¹ : Module ℝ W
X : Type u_2
inst✝¹⁰ : Vec R X
Y : Type u_3
inst✝⁹ : Vec R Y
inst✝⁸ : Module ℝ Y
Z : Type ?u.339803
inst✝⁷ : Vec R Z
U : Type ?u.339824
inst✝⁶ : Vec R U
V : Type ?u.339845
inst✝⁵ : Vec R V
inst✝⁴ : MeasureSpace X
X₁ : Type ?u.339869
inst✝³ : Vec R X₁
X₂ : Type ?u.339890
inst✝² : Vec R X₂
Y₁ : Type ?u.339911
inst✝¹ : Vec R Y₁
Y₂ : Type ?u.339932
inst✝ : Vec R Y₂
f : X → Y
φ : 𝒟 X
⊢ ↑f φ = ∫' x, φ x • f x
Tactic:
rfl
Proof state after:
no goals
Theorem: SciLean.Function.toDistribution_zero
Proof state before:
R : Type u_1
inst✝¹³ : RealScalar R
W : Type ?u.348494
inst✝¹² : Vec R W
inst✝¹¹ : Module ℝ W
X : Type u_2
inst✝¹⁰ : Vec R X
Y : Type u_3
inst✝⁹ : Vec R Y
inst✝⁸ : Module ℝ Y
Z : Type ?u.350103
inst✝⁷ : Vec R Z
U : Type ?u.350124
inst✝⁶ : Vec R U
V : Type ?u.350145
inst✝⁵ : Vec R V
inst✝⁴ : MeasureSpace X
X₁ : Type ?u.350169
inst✝³ : Vec R X₁
X₂ : Type ?u.350190
inst✝² : Vec R X₂
Y₁ : Type ?u.350211
inst✝¹ : Vec R Y₁
Y₂ : Type ?u.350232
inst✝ : Vec R Y₂
⊢ (↑fun x => 0) = 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.dpure_action
Proof state before:
R : Type ?u.9315
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
φ : X → ℝ
x dx : X
⊢ (dpure x dx).action φ = (fderiv ℝ φ x) dx
Tactic:
simp[Rand.dpure]
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.dpure_dE
Proof state before:
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ dE (dpure x dx) φ = (fderiv ℝ φ x) dx
Tactic:
simp only [bindRD,dE,dpure,rand_simp]
Proof state after:
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ testFunctionExtension (fun f => (fderiv ℝ f x) dx) φ = (fderiv ℝ φ x) dx
Theorem: SciLean.Prob.DRand.dpure_dE
Proof state before:
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ testFunctionExtension (fun f => (fderiv ℝ f x) dx) φ = (fderiv ℝ φ x) dx
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ ∀ (φ : X → ℝ) (y : Y), (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Theorem: SciLean.Prob.DRand.dpure_dE
Proof state before:
case h
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ ∀ (φ : X → ℝ) (y : Y), (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Tactic:
intro φ y
Proof state after:
case h
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ✝ : X → Y
φ : X → ℝ
y : Y
⊢ (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Theorem: SciLean.Prob.DRand.dpure_dE
Proof state before:
case h
R : Type ?u.14085
inst✝¹⁶ : RealScalar R
X : Type
inst✝¹⁵ : NormedAddCommGroup X
inst✝¹⁴ : NormedSpace ℝ X
inst✝¹³ : NormedSpace R X
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : NormedAddCommGroup Y
inst✝¹⁰ : NormedSpace ℝ Y
inst✝⁹ : NormedSpace R X
inst✝⁸ : MeasurableSpace Y
Z : Type
inst✝⁷ : NormedAddCommGroup Z
inst✝⁶ : NormedSpace ℝ Z
inst✝⁵ : NormedSpace R X
inst✝⁴ : MeasurableSpace Z
W : Type
inst✝³ : NormedAddCommGroup W
inst✝² : NormedSpace ℝ W
inst✝¹ : NormedSpace R X
inst✝ : MeasurableSpace W
x dx : X
φ✝ : X → Y
φ : X → ℝ
y : Y
⊢ (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Tactic:
simp (disch:=sorry) [fderiv_smul]
Proof state after:
no goals