internlm/Lean-Github huggingface dataset:
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w), dval := randDeriv Rand.pure (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
rw [Rand.pure.arg_x.randDeriv_rule _ differentiable_id']
Proof state after:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w),
      dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3044
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3161
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3278
inst✝¹ : MeasurableSpace α
β : Type ?u.3284
inst✝ : MeasurableSpace β
x : W → X
hx : Differentiable ℝ x
w dw : W
⊢ { val := Rand.pure (x w),
      dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) (x w) ((fderiv ℝ (fun x_1 => x x_1) w) dw) } =
    { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
simp
Proof state after:
no goals
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple
Proof state before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (randFwdDeriv fun x => Rand.pure x) = fun x dx => fdpure x dx
Tactic:
unfold randFwdDeriv fdpure
Proof state after:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => Rand.pure x) x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple
Proof state before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := (fun x => Rand.pure x) x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Tactic:
simp (disch:=first | apply hx | sorry) [rand_simp]
Proof state after:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := Rand.pure x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple
Proof state before:
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
⊢ (fun x dx => { val := Rand.pure x, dval := randDeriv (fun x => Rand.pure x) x dx }) = fun x dx =>
    { val := Rand.pure x, dval := dpure x dx }
Tactic:
funext w dw
Proof state after:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := randDeriv (fun x => Rand.pure x) w dw } = { val := Rand.pure w, dval := dpure w dw }
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple
Proof state before:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := randDeriv (fun x => Rand.pure x) w dw } = { val := Rand.pure w, dval := dpure w dw }
Tactic:
rw [Rand.pure.arg_x.randDeriv_rule _ differentiable_id']
Proof state after:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) w dw } =
    { val := Rand.pure w, dval := dpure w dw }
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule_simple
Proof state before:
case h.h
W : Type ?u.8184
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.8419
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.8536
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.8653
inst✝¹ : MeasurableSpace α
β : Type ?u.8659
inst✝ : MeasurableSpace β
w dw : X
⊢ { val := Rand.pure w, dval := (fun w dw => dpure w ((fderiv ℝ (fun x => x) w) dw)) w dw } =
    { val := Rand.pure w, dval := dpure w dw }
Tactic:
simp (disch:=first | apply hx | sorry) [rand_simp]
Proof state after:
no goals
Theorem: Probly.Rand.bind.arg_xf.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
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
⊢ (randFwdDeriv fun w =>
      let x ~ x w
      f w x) =
    fun w dw =>
    let x ~~ randFwdDeriv x w dw
    randFwdDeriv (fun x_1 => f x_1 x) w dw
Tactic:
unfold randFwdDeriv FDRand.bind
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
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
⊢ (fun x_1 dx =>
      {
        val :=
          (fun w =>
              let x ~ x w
              f w x)
            x_1,
        dval :=
          randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            x_1 dx }) =
    fun w dw =>
    {
      val :=
        let x' ~ { val := x w, dval := randDeriv x w dw }.val
        ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val,
      dval :=
        (DRand.bindDR { val := x w, dval := randDeriv x w dw }.dval fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val) +
          bindRD { val := x w, dval := randDeriv x w dw }.val fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').dval }
Theorem: Probly.Rand.bind.arg_xf.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.12957
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.13074
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.13191
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
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
⊢ (fun x_1 dx =>
      {
        val :=
          (fun w =>
              let x ~ x w
              f w x)
            x_1,
        dval :=
          randDeriv
            (fun w =>
              let x ~ x w
              f w x)
            x_1 dx }) =
    fun w dw =>
    {
      val :=
        let x' ~ { val := x w, dval := randDeriv x w dw }.val
        ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val,
      dval :=
        (DRand.bindDR { val := x w, dval := randDeriv x w dw }.dval fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').val) +
          bindRD { val := x w, dval := randDeriv x w dw }.val fun x' =>
            ((fun x => { val := (fun x_1 => f x_1 x) w, dval := randDeriv (fun x_1 => f x_1 x) w dw }) x').dval }
Tactic:
simp (disch:=first | apply hx | apply hf) only [rand_simp]
Proof state after:
no goals
Theorem: Probly.ite.arg_tf.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: Probly.ite.arg_tf.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
h : c
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Probly.ite.arg_tf.randFwdDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.14943
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.15060
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.15177
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.15300
inst✝¹ : MeasurableSpace β
c : Prop
inst✝ : Decidable c
t f : W → Rand α
h : ¬c
⊢ (randFwdDeriv fun w => if c then t w else f w) = fun w dw => if c then randFwdDeriv t w dw else randFwdDeriv f w dw
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Probly.DRand.dpure_action
Proof state before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
φ : X → ℝ
x dx : X
⊢ (dpure x dx).action φ = (fderiv ℝ φ x) dx
Tactic:
simp[Rand.dpure]
Proof state after:
no goals
Theorem: Probly.DRand.dpure_dE
Proof state before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
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:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ testFunctionExtension (fun f => (fderiv ℝ f x) dx) φ = (fderiv ℝ φ x) dx
Theorem: Probly.DRand.dpure_dE
Proof state before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
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
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x dx : X
φ : X → Y
⊢ ∀ (φ : X → ℝ) (y : Y), (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Theorem: Probly.DRand.dpure_dE
Proof state before:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
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
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x dx : X
φ✝ : X → Y
φ : X → ℝ
y : Y
⊢ (fderiv ℝ φ x) dx • y = (fderiv ℝ (fun x => φ x • y) x) dx
Theorem: Probly.DRand.dpure_dE
Proof state before:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
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
Theorem: Probly.DRand.bindRD_dE
Proof state before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ : Y → Z
⊢ dE (bindRD x f) φ = E x fun x' => dE (f x') φ
Tactic:
simp only [bindRD,dE,rand_simp,E,expectedValue]
Proof state after:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => ∫ (x' : X), (f x').action φ ∂↑x.μ) φ =
    ∫ (x' : X), testFunctionExtension (f x').action φ ∂↑x.μ
Theorem: Probly.DRand.bindRD_dE
Proof state before:
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => ∫ (x' : X), (f x').action φ ∂↑x.μ) φ =
    ∫ (x' : X), testFunctionExtension (f x').action φ ∂↑x.μ
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), testFunctionExtension (f x').action fun x => φ x • y ∂↑x.μ
Theorem: Probly.DRand.bindRD_dE
Proof state before:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), testFunctionExtension (f x').action fun x => φ x • y ∂↑x.μ
Tactic:
intro φ y
Proof state after:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), testFunctionExtension (f x').action fun x => φ x • y ∂↑x.μ
Theorem: Probly.DRand.bindRD_dE
Proof state before:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), testFunctionExtension (f x').action fun x => φ x • y ∂↑x.μ
Tactic:
simp only [testFunctionExtension_test_function]
Proof state after:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), ((f x').action fun x => φ x) • y ∂↑x.μ
Theorem: Probly.DRand.bindRD_dE
Proof state before:
case h
X : Type
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
W : Type
inst✝² : NormedAddCommGroup W
inst✝¹ : NormedSpace ℝ W
inst✝ : MeasurableSpace W
x : Rand X
f : X → DRand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (∫ (x' : X), (f x').action φ ∂↑x.μ) • y = ∫ (x' : X), ((f x').action fun x => φ x) • y ∂↑x.μ
Tactic:
sorry
Proof state after:
no goals