Theorem: Probly.DRand.bindDR_dE (Probly/DRand.lean)

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 : 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,expectedValue]
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 : 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').μ

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 : 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
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 : 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').μ

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 : 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
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 : 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').μ

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 : 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
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 : 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

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 : 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
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 : 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

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 : 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
State after:
no goals