internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
⊢ (randDeriv fun w =>
      let x ~ x w
      f w x) =
    fun w dw =>
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw
Tactic:
funext w dw
Proof state after:
case h.h
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
⊢ randDeriv
      (fun w =>
        let x ~ x w
        f w x)
      w dw =
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
⊢ randDeriv
      (fun w =>
        let x ~ x w
        f w x)
      w dw =
    (DRand.bindDR (randDeriv x w dw) fun x => f w x) + bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw
Tactic:
apply DRand.ext
Proof state after:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
⊢ ∀ (φ : β → ℝ),
    (randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            w dw).action
        φ =
      ((DRand.bindDR (randDeriv x w dw) fun x => f w x) +
            bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw).action
        φ
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
⊢ ∀ (φ : β → ℝ),
    (randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            w dw).action
        φ =
      ((DRand.bindDR (randDeriv x w dw) fun x => f w x) +
            bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw).action
        φ
Tactic:
intro φ
Proof state after:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (randDeriv
          (fun w =>
            let x ~ x w
            f w x)
          w dw).action
      φ =
    ((DRand.bindDR (randDeriv x w dw) fun x => f w x) +
          bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw).action
      φ
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (randDeriv
          (fun w =>
            let x ~ x w
            f w x)
          w dw).action
      φ =
    ((DRand.bindDR (randDeriv x w dw) fun x => f w x) +
          bindRD (x w) fun x => randDeriv (fun x_1 => f x_1 x) w dw).action
      φ
Tactic:
simp only [randDeriv, rand_simp, DRand.bindDR, bindRD, E]
Proof state after:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (fderiv ℝ
        (fun x' =>
          ∫ (y : β),
            φ y ∂↑(let x ~ x x'
                f x' x).μ)
        w)
      dw =
    (fderiv ℝ (fun x' => ∫ (y : α), ∫ (y : β), φ y ∂↑(f w y).μ ∂↑(x x').μ) w) dw +
      ∫ (x' : α), (fderiv ℝ (fun x'_1 => ∫ (y : β), φ y ∂↑(f x'_1 x').μ) w) dw ∂↑(x w).μ
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (fderiv ℝ
        (fun x' =>
          ∫ (y : β),
            φ y ∂↑(let x ~ x x'
                f x' x).μ)
        w)
      dw =
    (fderiv ℝ (fun x' => ∫ (y : α), ∫ (y : β), φ y ∂↑(f w y).μ ∂↑(x x').μ) w) dw +
      ∫ (x' : α), (fderiv ℝ (fun x'_1 => ∫ (y : β), φ y ∂↑(f x'_1 x').μ) w) dw ∂↑(x w).μ
Tactic:
simp (disch:=sorry) only [integral_bind]
Proof state after:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (fderiv ℝ (fun x' => ∫ (x'_1 : α), ∫ (y : β), φ y ∂↑(f x' x'_1).μ ∂↑(x x').μ) w) dw =
    (fderiv ℝ (fun x' => ∫ (y : α), ∫ (y : β), φ y ∂↑(f w y).μ ∂↑(x x').μ) w) dw +
      ∫ (x' : α), (fderiv ℝ (fun x'_1 => ∫ (y : β), φ y ∂↑(f x'_1 x').μ) w) dw ∂↑(x w).μ
Theorem: SciLean.Prob.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
R : Type ?u.24924
inst✝¹⁸ : RealScalar R
W : Type u_1
inst✝¹⁷ : NormedAddCommGroup W
inst✝¹⁶ : NormedSpace ℝ W
inst✝¹⁵ : NormedSpace R W
inst✝¹⁴ : MeasurableSpace W
X : Type ?u.25180
inst✝¹³ : NormedAddCommGroup X
inst✝¹² : NormedSpace ℝ X
inst✝¹¹ : NormedSpace R W
inst✝¹⁰ : MeasurableSpace X
Y : Type ?u.25419
inst✝⁹ : NormedAddCommGroup Y
inst✝⁸ : NormedSpace ℝ Y
inst✝⁷ : NormedSpace R W
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.25658
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : NormedSpace R W
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type
inst✝ : MeasurableSpace β
x : W → Rand α
f : W → α → Rand β
hx : RandDifferentiable x
hf : ∀ (x : α), RandDifferentiable fun x_1 => f x_1 x
w dw : W
φ : β → ℝ
⊢ (fderiv ℝ (fun x' => ∫ (x'_1 : α), ∫ (y : β), φ y ∂↑(f x' x'_1).μ ∂↑(x x').μ) w) dw =
    (fderiv ℝ (fun x' => ∫ (y : α), ∫ (y : β), φ y ∂↑(f w y).μ ∂↑(x x').μ) w) dw +
      ∫ (x' : α), (fderiv ℝ (fun x'_1 => ∫ (y : β), φ y ∂↑(f x'_1 x').μ) w) dw ∂↑(x w).μ
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_tf.randDeriv_rule
Proof state before:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
⊢ (randDeriv fun w => if c then t w else f w) = fun w dw => if c then randDeriv t w dw else randDeriv f w dw
Tactic:
funext w dw
Proof state after:
case h.h
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
Theorem: SciLean.Prob.ite.arg_tf.randDeriv_rule
Proof state before:
case h.h
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
Tactic:
if h : c then simp [h] else simp [h]
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_tf.randDeriv_rule
Proof state before:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
h : c
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
Tactic:
simp [h]
Proof state after:
no goals
Theorem: SciLean.Prob.ite.arg_tf.randDeriv_rule
Proof state before:
R : Type ?u.28081
inst✝¹⁹ : RealScalar R
W : Type u_1
inst✝¹⁸ : NormedAddCommGroup W
inst✝¹⁷ : NormedSpace ℝ W
inst✝¹⁶ : NormedSpace R W
inst✝¹⁵ : MeasurableSpace W
X : Type ?u.28337
inst✝¹⁴ : NormedAddCommGroup X
inst✝¹³ : NormedSpace ℝ X
inst✝¹² : NormedSpace R W
inst✝¹¹ : MeasurableSpace X
Y : Type ?u.28576
inst✝¹⁰ : NormedAddCommGroup Y
inst✝⁹ : NormedSpace ℝ Y
inst✝⁸ : NormedSpace R W
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.28815
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace ℝ Z
inst✝⁴ : NormedSpace R W
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.29060
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
w dw : W
h : ¬c
⊢ randDeriv (fun w => if c then t w else f w) w dw = if c then randDeriv t w dw else randDeriv f w dw
Tactic:
simp [h]
Proof state after:
no goals
Theorem: IsLinearMap.isLinearMap_const_zero
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.6113
ι : Type ?u.6116
E : ι → Type ?u.6121
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ IsLinearMap R fun x => 0
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsLinearMap.isLinearMap_apply
Proof state before:
R : Type u_1
X : Type ?u.16164
Y : Type ?u.16167
Z : Type ?u.16170
ι : Type u_2
E : ι → Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
i : ι
⊢ IsLinearMap R fun f => f i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: IsLinearMap.isLinearMap_pi
Proof state before:
R : Type u_1
X : Type u_2
Y : Type ?u.18207
Z : Type ?u.18210
ι : Type u_4
E : ι → Type u_3
inst✝⁸ : Semiring R
inst✝⁷ : AddCommGroup X
inst✝⁶ : Module R X
inst✝⁵ : AddCommGroup Y
inst✝⁴ : Module R Y
inst✝³ : AddCommGroup Z
inst✝² : Module R Z
inst✝¹ : (i : ι) → AddCommMonoid (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → (i : ι) → E i
hf : ∀ (i : ι), IsLinearMap R fun x => f x i
⊢ IsLinearMap R fun x i => f x i
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: Prod.mk.arg_fstsnd.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_4
Z : Type u_3
ι : Type ?u.47164
E : ι → Type ?u.47169
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Z
g : X → Y
hf : IsLinearMap R f
hg : IsLinearMap R g
⊢ ∀ (x : X), (g x, f x) = (LinearMap.prod (mk' g hg) (mk' f hf)) x
Tactic:
simp
Proof state after:
no goals
Theorem: Prod.fst.arg_self.IsLinearMap_rule
Proof state before:
R : Type u_3
X : Type u_4
Y : Type u_1
Z : Type u_2
ι : Type ?u.59699
E : ι → Type ?u.59704
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y × Z
hf : IsLinearMap R f
⊢ ∀ (x : X), (f x).1 = (LinearMap.fst R Y Z ∘ₗ mk' f hf) x
Tactic:
simp
Proof state after:
no goals
Theorem: Prod.fst.arg_self.IsLinearMap_rule_simple
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.74692
ι : Type ?u.74695
E : ι → Type ?u.74700
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ IsLinearMap R fun xy => xy.1
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Prod.snd.arg_self.IsLinearMap_rule
Proof state before:
R : Type u_3
X : Type u_4
Y : Type u_1
Z : Type u_2
ι : Type ?u.80255
E : ι → Type ?u.80260
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y × Z
hf : IsLinearMap R f
⊢ ∀ (x : X), (f x).2 = (LinearMap.snd R Y Z ∘ₗ mk' f hf) x
Tactic:
simp
Proof state after:
no goals
Theorem: Prod.snd.arg_self.IsLinearMap_rule_simple
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.94338
ι : Type ?u.94341
E : ι → Type ?u.94346
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ IsLinearMap R fun xy => xy.2
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Prod.mk.arg_fstsnd.IsLinearMap_rule_simple
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.99898
ι : Type ?u.99901
E : ι → Type ?u.99906
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
⊢ IsLinearMap R fun xy => (xy.1, xy.2)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: Neg.neg.arg_a0.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.106079
ι : Type ?u.106082
E : ι → Type ?u.106087
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → Y
hf : IsLinearMap R f
⊢ ∀ (x : X), -f x = (-mk' f hf) x
Tactic:
simp
Proof state after:
no goals
Theorem: HAdd.hAdd.arg_a0a1.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.115787
ι : Type ?u.115790
E : ι → Type ?u.115795
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f g : X → Y
hf : IsLinearMap R f
hg : IsLinearMap R g
⊢ ∀ (x : X), f x + g x = (mk' f hf + mk' g hg) x
Tactic:
simp
Proof state after:
no goals
Theorem: HSub.hSub.arg_a0a1.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.125989
ι : Type ?u.125992
E : ι → Type ?u.125997
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f g : X → Y
hf : IsLinearMap R f
hg : IsLinearMap R g
⊢ ∀ (x : X), f x - g x = (mk' f hf - mk' g hg) x
Tactic:
simp
Proof state after:
no goals
Theorem: HSMul.hSMul.arg_a0.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.137944
ι : Type ?u.137947
E : ι → Type ?u.137952
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → R
y : Y
hf : IsLinearMap R f
a : R →ₗ[R] Y := mk' (fun c => c • y) ⋯
b : X →ₗ[R] R := mk' f hf
⊢ ∀ (x : X), f x • y = (a ∘ₗ b) x
Tactic:
simp (config:={zetaDelta:=true})
Proof state after:
no goals
Theorem: IndexType.sum.arg_f.IsLinearMap_rule
Proof state before:
R : Type u_1
X : Type u_2
Y : Type u_3
Z : Type ?u.160652
ι : Type u_4
E : ι → Type ?u.160660
inst✝¹¹ : Semiring R
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module R X
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module R Y
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module R Z
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module R (E i)
f : X → ι → Y
hf : ∀ (i : ι), IsLinearMap R fun x => f x i
⊢ IsLinearMap R fun x =>  ∑ i, f x i
Tactic:
sorry_proof
Proof state after:
no goals