internlm/Lean-Github huggingface dataset:
Theorem: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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, expectedValue]
Proof state after:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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: Probly.Rand.bind.arg_xf.randDeriv_rule
Proof state before:
case h.h.a
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.24859
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.24976
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.25093
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
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: Probly.ite.arg_tf.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
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
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
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: Probly.ite.arg_tf.randDeriv_rule
Proof state before:
case h.h
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
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: Probly.ite.arg_tf.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
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: Probly.ite.arg_tf.randDeriv_rule
Proof state before:
W : Type u_1
inst✝¹⁴ : NormedAddCommGroup W
inst✝¹³ : NormedSpace ℝ W
inst✝¹² : MeasurableSpace W
X : Type ?u.27651
inst✝¹¹ : NormedAddCommGroup X
inst✝¹⁰ : NormedSpace ℝ X
inst✝⁹ : MeasurableSpace X
Y : Type ?u.27768
inst✝⁸ : NormedAddCommGroup Y
inst✝⁷ : NormedSpace ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.27885
inst✝⁵ : NormedAddCommGroup Z
inst✝⁴ : NormedSpace ℝ Z
inst✝³ : MeasurableSpace Z
α : Type
inst✝² : MeasurableSpace α
β : Type ?u.28008
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: Probly.weightByDensity'_bind
Proof state before:
X : Type
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : MeasurableSpace X
Y : Type ?u.1340
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : MeasurableSpace Y
Z : Type ?u.1457
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : MeasurableSpace Z
p q : ℝ
x : Rand (X × X)
⊢ (let x' ~ x
    Rand.pure (weightByDensity' p q x')) =
    weightByDensityM' p q x
Tactic:
rfl
Proof state after:
no goals
Theorem: Probly.ite_push_fdE
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 ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
if h : c then simp[h] else simp[h]
Proof state after:
no goals
Theorem: Probly.ite_push_fdE
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 ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
h : c
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Probly.ite_push_fdE
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 ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
h : ¬c
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
Tactic:
simp[h]
Proof state after:
no goals
Theorem: Probly.uniform.arg_ab.randFwdDeriv_rule
Proof state before:
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
⊢ (randFwdDeriv fun w => uniform (a w) (b w)) = fun w dw =>
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2
Tactic:
funext w dw
Proof state after:
case h.h
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
w dw : W
⊢ randFwdDeriv (fun w => uniform (a w) (b w)) w dw =
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2
Theorem: Probly.uniform.arg_ab.randFwdDeriv_rule
Proof state before:
case h.h
a✝ b✝ : ℝ
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.2943
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.3060
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.3177
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.3294
inst✝¹ : MeasurableSpace α
β : Type ?u.3300
inst✝ : MeasurableSpace β
a b : W → ℝ
ha : Differentiable ℝ a
hb : Differentiable ℝ b
w dw : W
⊢ randFwdDeriv (fun w => uniform (a w) (b w)) w dw =
    let ada := fwdDeriv ℝ a w dw;
    let bdb := fwdDeriv ℝ b w dw;
    fduniform ada.1 bdb.1 ada.2 bdb.2
Tactic:
simp (disch:=sorry) [randFwdDeriv,fwdDeriv,fduniform]
Proof state after:
no goals
Theorem: Probly.FDRand.bind_bind
Proof state before:
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ bind (bind x g) f = bind x fun x' => bind (g x') f
Tactic:
apply ext
Proof state after:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val

case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Theorem: Probly.FDRand.bind_bind
Proof state before:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val

case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Theorem: Probly.FDRand.bind_bind
Proof state before:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
. simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals
Theorem: Probly.FDRand.bind_bind
Proof state before:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).val = (bind x fun x' => bind (g x') f).val
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals
Theorem: Probly.FDRand.bind_bind
Proof state before:
case a
X✝ : Type ?u.5449
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.5567
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.5684
inst✝¹⁴ : NormedAddCommGroup Z✝
inst✝¹³ : NormedSpace ℝ Z✝
inst✝¹² : MeasurableSpace Z✝
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 : FDRand X
g : X → FDRand Y
f : Y → FDRand Z
⊢ (bind (bind x g) f).dval = (bind (bind x g) f).dval
Tactic:
simp (disch:=sorry) only [bind,rand_simp]
Proof state after:
no goals