internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Prob.DRand.bindRD_dE
Proof state before:
R : Type ?u.23564
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 : 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]
Proof state after:
R : Type ?u.23564
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 : Rand X
f : X → DRand Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => ∫ (x' : X), (f x').action φ ∂↑x.μ) φ =
    ∫ (x' : X), testFunctionExtension (f x').action φ ∂↑x.μ
Theorem: SciLean.Prob.DRand.bindRD_dE
Proof state before:
R : Type ?u.23564
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 : 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
R : Type ?u.23564
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 : 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: SciLean.Prob.DRand.bindRD_dE
Proof state before:
case h
R : Type ?u.23564
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 : 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
R : Type ?u.23564
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 : 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: SciLean.Prob.DRand.bindRD_dE
Proof state before:
case h
R : Type ?u.23564
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 : 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
R : Type ?u.23564
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 : 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: SciLean.Prob.DRand.bindRD_dE
Proof state before:
case h
R : Type ?u.23564
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 : 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
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ : Y → Z
⊢ dE (bindDR x f) φ = dE x fun x' => E (f x') φ
Tactic:
simp only [bindDR,dE,rand_simp, E]
Proof state after:
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) φ =
    testFunctionExtension x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) φ =
    testFunctionExtension x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y =
      testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y =
      testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ
Tactic:
intro φ y
Proof state after:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y =
    testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y =
    testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ
Tactic:
symm
Proof state after:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ) =
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => ∫ (x' : Y), (fun x => φ x • y) x' ∂↑(f x').μ) =
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y
Tactic:
dsimp
Proof state after:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => ∫ (x' : Y), φ x' • y ∂↑(f x').μ) =
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y
Theorem: SciLean.Prob.DRand.bindDR_dE
Proof state before:
case h
R : Type ?u.25112
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 : DRand X
f : X → Rand Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => ∫ (x' : Y), φ x' • y ∂↑(f x').μ) =
    (x.action fun x' => ∫ (x' : Y), φ x' ∂↑(f x').μ) • y
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
R : Type ?u.26702
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 : DRand X
f : X → Y
φ : Y → Z
⊢ dE (bindDR x fun x' => Rand.pure (f x')) φ = dE x fun x' => φ (f x')
Tactic:
simp only [bindDR,dE,rand_simp]
Proof state after:
R : Type ?u.26702
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 : DRand X
f : X → Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => x.action fun x' => φ (f x')) φ = testFunctionExtension x.action fun x' => φ (f x')
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
R : Type ?u.26702
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 : DRand X
f : X → Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => x.action fun x' => φ (f x')) φ = testFunctionExtension x.action fun x' => φ (f x')
Tactic:
apply testFunctionExtension_ext
Proof state after:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (x.action fun x' => φ (f x')) • y = testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ : Y → Z
⊢ ∀ (φ : Y → ℝ) (y : Z),
    (x.action fun x' => φ (f x')) • y = testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')
Tactic:
intro φ y
Proof state after:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (x.action fun x' => φ (f x')) • y = testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (x.action fun x' => φ (f x')) • y = testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')
Tactic:
symm
Proof state after:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')) = (x.action fun x' => φ (f x')) • y
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => (fun x => φ x • y) (f x')) = (x.action fun x' => φ (f x')) • y
Tactic:
dsimp
Proof state after:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => φ (f x') • y) = (x.action fun x' => φ (f x')) • y
Theorem: SciLean.Prob.DRand.bindDR_pure
Proof state before:
case h
R : Type ?u.26702
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 : DRand X
f : X → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => φ (f x') • y) = (x.action fun x' => φ (f x')) • y
Tactic:
rw[testFunctionExtension_test_function]
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.pure_bindRD
Proof state before:
R : Type ?u.28617
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
f : X → DRand Y
⊢ bindRD (Rand.pure x) f = f x
Tactic:
simp only [bindRD,dE,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.DRand.bindRD_dpure
Proof state before:
R : Type ?u.29780
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 : Rand X
f df : X → Y
φ : Y → Z
⊢ dE (bindRD x fun x' => dpure (f x') (df x')) φ = E x fun x' => (fderiv ℝ φ (f x')) (df x')
Tactic:
simp only [rand_simp]
Proof state after:
no goals