internlm/Lean-Github huggingface dataset:
Theorem: Probly.DRand.bindDR_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 : 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]
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 : 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: Probly.DRand.bindDR_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 : 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
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').μ
Theorem: Probly.DRand.bindDR_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 : 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
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').μ
Theorem: Probly.DRand.bindDR_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 : 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
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
Theorem: Probly.DRand.bindDR_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 : 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
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
Theorem: Probly.DRand.bindDR_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 : 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: Probly.DRand.bindDR_pure
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 : 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:
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 → Y
φ : Y → Z
⊢ testFunctionExtension (fun φ => x.action fun x' => φ (f x')) φ = testFunctionExtension x.action fun x' => φ (f x')
Theorem: Probly.DRand.bindDR_pure
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 : 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
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 → 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: Probly.DRand.bindDR_pure
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 : 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
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 → 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: Probly.DRand.bindDR_pure
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 : 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
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 → 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: Probly.DRand.bindDR_pure
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 : 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
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 → Y
φ✝ : Y → Z
φ : Y → ℝ
y : Z
⊢ (testFunctionExtension x.action fun x' => φ (f x') • y) = (x.action fun x' => φ (f x')) • y
Theorem: Probly.DRand.bindDR_pure
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 : 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: Probly.DRand.pure_bindRD
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
f : X → DRand Y
⊢ bindRD (Rand.pure x) f = f x
Tactic:
simp only [bindRD,dE,rand_simp]
Proof state after:
no goals
Theorem: Probly.DRand.bindRD_dpure
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 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
Theorem: Probly.DRand.dpure_bindDR
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
f : X → Rand Y
⊢ bindDR (dpure x dx) f = randDeriv f x dx
Tactic:
apply ext
Proof state after:
case a
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
f : X → Rand Y
⊢ ∀ (φ : Y → ℝ), (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Theorem: Probly.DRand.dpure_bindDR
Proof state before:
case a
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
f : X → Rand Y
⊢ ∀ (φ : Y → ℝ), (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Tactic:
intro φ
Proof state after:
case a
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
f : X → Rand Y
φ : Y → ℝ
⊢ (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Theorem: Probly.DRand.dpure_bindDR
Proof state before:
case a
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
f : X → Rand Y
φ : Y → ℝ
⊢ (bindDR (dpure x dx) f).action φ = (randDeriv f x dx).action φ
Tactic:
simp only [bindDR, dpure, dE, randDeriv,E,expectedValue]
Proof state after:
no goals
Theorem: Probly.DRand.bindDR_bindDR
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 : DRand X
g : X → Rand Y
f : Y → Rand Z
⊢ bindDR (bindDR x g) f = bindDR x fun x' => Rand.bind (g x') f
Tactic:
simp (disch:=sorry) only [bindDR,rand_simp,rand_push_E]
Proof state after:
no goals
Theorem: Probly.DRand.bindRD_bindDR
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
g : X → DRand Y
f : Y → Rand Z
⊢ bindDR (bindRD x g) f = bindRD x fun x' => bindDR (g x') f
Tactic:
simp (disch:=sorry) only [bindDR,bindRD,rand_simp]
Proof state after:
no goals
Theorem: not_differentiableAt_abs
Proof state before:
⊢ ¬DifferentiableAt ℝ (fun x => |x|) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: C02S04.aux
Proof state before:
a b c d : ℝ
⊢ min a b + c ≤ min (a + c) (b + c)
Tactic:
sorry
Proof state after:
no goals
Theorem: inverse_of_a_commutator
Proof state before:
G : Type
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆⁻¹ = ⁅h, g⁆
Tactic:
sorry
Proof state after:
no goals
Theorem: simple_proof
Proof state before:
G : Type
inst✝¹ : Group G
g h : G
R : Type
inst✝ : CommRing R
a b : R
p q r : Prop
h1 : p → q
h2 : q → r
⊢ p → r
Tactic:
sorry
Proof state after:
no goals
Theorem: TopologySession.Tendsto_iff
Proof state before:
X✝ : Type ?u.2133
Y✝ : Type ?u.2136
X : Type u_1
Y : Type u_2
f : X → Y
F : Filter X
G : Filter Y
⊢ Tendsto f F G ↔ ∀ (S : Set Y), S ∈ G → f ⁻¹' S ∈ F
Tactic:
rfl
Proof state after:
no goals
Theorem: MyDefs.Set.ext
Proof state before:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
s t : Set α
⊢ s = t → ∀ (x : α), x ∈ s ↔ x ∈ t

case mpr
α : Type u_1
s t : Set α
⊢ (∀ (x : α), x ∈ s ↔ x ∈ t) → s = t
Theorem: MyDefs.Set.ext
Proof state before:
case mp
α : Type u_1
s t : Set α
⊢ s = t → ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
intro h x
Proof state after:
case mp
α : Type u_1
s t : Set α
h : s = t
x : α
⊢ x ∈ s ↔ x ∈ t
Theorem: MyDefs.Set.ext
Proof state before:
case mp
α : Type u_1
s t : Set α
h : s = t
x : α
⊢ x ∈ s ↔ x ∈ t
Tactic:
rw [h]
Proof state after:
no goals
Theorem: MyDefs.Set.ext
Proof state before:
case mpr
α : Type u_1
s t : Set α
⊢ (∀ (x : α), x ∈ s ↔ x ∈ t) → s = t
Tactic:
intro h
Proof state after:
case mpr
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
⊢ s = t
Theorem: MyDefs.Set.ext
Proof state before:
case mpr
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
⊢ s = t
Tactic:
funext x
Proof state after:
case mpr.h
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x = t x
Theorem: MyDefs.Set.ext
Proof state before:
case mpr.h
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x = t x
Tactic:
apply propext
Proof state after:
case mpr.h.a
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x ↔ t x
Theorem: MyDefs.Set.ext
Proof state before:
case mpr.h.a
α : Type u_1
s t : Set α
h : ∀ (x : α), x ∈ s ↔ x ∈ t
x : α
⊢ s x ↔ t x
Tactic:
exact h x
Proof state after:
no goals
Theorem: MyDefs.Set.ext'
Proof state before:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t
Tactic:
conv =>
  rhs
  ext
  rw [← eq_iff_iff]
Proof state after:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), (x ∈ s) = (x ∈ t)
Theorem: MyDefs.Set.ext'
Proof state before:
α : Type u_1
s t : Set α
⊢ s = t ↔ ∀ (x : α), (x ∈ s) = (x ∈ t)
Tactic:
exact Function.funext_iff
Proof state after:
no goals
Theorem: cauchySeq_of_le_geometric_two'
Proof state before:
case h.intro
X : Type u_1
inst✝ : MetricSpace X
a b c : X
r : ℝ
u : ℕ → X
hu : ∀ (n : ℕ), dist (u n) (u (n + 1)) ≤ (1 / 2) ^ n
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : 1 / 2 ^ N * 2 < ε
k : ℕ
hn : N + k ≥ N
⊢ dist (u (N + k)) (u N) < ε
Tactic:
calc
  dist (u (N + k)) (u N) = dist (u (N + 0)) (u (N + k)) := sorry
  _ ≤ ∑ i in range k, dist (u (N + i)) (u (N + (i + 1))) := sorry
  _ ≤ ∑ i in range k, (1 / 2 : ℝ) ^ (N + i) := sorry
  _ = 1 / 2 ^ N * ∑ i in range k, (1 / 2) ^ i := sorry
  _ ≤ 1 / 2 ^ N * 2 := sorry
  _ < ε := sorry
Proof state after:
no goals
Theorem: absorb1
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) = x
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) ≤ x

case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊓ (x ⊔ y)
Theorem: absorb1
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊓ (x ⊔ y)
Tactic:
apply le_inf
Proof state after:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x

case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ y
Theorem: absorb1
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ y
Tactic:
apply le_sup_left
Proof state after:
no goals
Theorem: absorb1
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ (x ⊔ y) ≤ x
Tactic:
apply inf_le_left
Proof state after:
no goals
Theorem: absorb1
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: absorb2
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y = x
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x

case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y
Theorem: absorb2
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x ⊔ x ⊓ y
Tactic:
apply le_sup_left
Proof state after:
no goals
Theorem: absorb2
Proof state before:
case a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊔ x ⊓ y ≤ x
Tactic:
apply sup_le
Proof state after:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x

case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ y ≤ x
Theorem: absorb2
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ⊓ y ≤ x
Tactic:
apply inf_le_left
Proof state after:
no goals
Theorem: absorb2
Proof state before:
case a.a
α : Type u_1
inst✝ : Lattice α
x y z : α
⊢ x ≤ x
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: Language.concat_assoc
Proof state before:
α : Type u_1
X Y Z : Language α
⊢ X ∘ₗ Y ∘ₗ Z = X ∘ₗ (Y ∘ₗ Z)
Tactic:
apply Set.ext
Proof state after:
case h
α : Type u_1
X Y Z : Language α
⊢ ∀ (x : Word α), x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Theorem: Language.concat_assoc
Proof state before:
case h
α : Type u_1
X Y Z : Language α
⊢ ∀ (x : Word α), x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
intro x
Proof state after:
case h
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Theorem: Language.concat_assoc
Proof state before:
case h
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z ↔ x ∈ X ∘ₗ (Y ∘ₗ Z)
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ Y ∘ₗ Z → x ∈ X ∘ₗ (Y ∘ₗ Z)

case h.mpr
α : Type u_1
X Y Z : Language α
x : Word α
⊢ x ∈ X ∘ₗ (Y ∘ₗ Z) → x ∈ X ∘ₗ Y ∘ₗ Z