internlm/Lean-Github huggingface dataset:
Theorem: Probly.FDRand.FDRand_mk_fdE
Proof state before:
X✝ : Type ?u.23419
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.23537
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.23654
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 : Rand X
dx : DRand X
φ : X → Y
⊢ fdE { val := x, dval := dx } φ = (E x φ, DRand.dE dx φ)
Tactic:
rfl
Proof state after:
no goals
Theorem: Probly.FDRand.expectedValueAndChange_as_fdmean
Proof state before:
X✝ : Type ?u.36399
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.36517
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.36634
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
φ : X → Y
⊢ fdE x φ =
    fdmean
      (let x' ~~ x
      fdpure (φ x') 0)
Tactic:
simp (disch:=sorry) only [rand_simp,mean,fdE,fdmean,bind,fdpure,id]
Proof state after:
X✝ : Type ?u.36399
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.36517
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.36634
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
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)
Theorem: Probly.FDRand.expectedValueAndChange_as_fdmean
Proof state before:
X✝ : Type ?u.36399
inst✝²⁰ : NormedAddCommGroup X✝
inst✝¹⁹ : NormedSpace ℝ X✝
inst✝¹⁸ : MeasurableSpace X✝
Y✝ : Type ?u.36517
inst✝¹⁷ : NormedAddCommGroup Y✝
inst✝¹⁶ : NormedSpace ℝ Y✝
inst✝¹⁵ : MeasurableSpace Y✝
Z✝ : Type ?u.36634
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
φ : X → Y
⊢ (E x.val φ, DRand.dE x.dval φ) =
    (E
        (let x' ~ x.val
        Rand.pure (φ x'))
        id,
      (DRand.dE x.dval fun x' => φ x') + E x.val fun x' => (fderiv ℝ id (φ x')) 0)
Tactic:
simp
Proof state after:
no goals
Theorem: Probly.Rand.bind_probability
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2311
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
Tactic:
have := is_measurable hf
Proof state after:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2311
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
this : Measurable fun x => ↑(f x).μ
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
Theorem: Probly.Rand.bind_probability
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2311
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
s : Set Y
hs : MeasurableSet s
hf : Measurable f
this : Measurable fun x => ↑(f x).μ
⊢ probability (bind x f) s = ∫⁻ (x' : X), probability (f x') s ∂↑x.μ
Tactic:
simp (disch:=assumption) [bind, probability, Measure.bind_apply]
Proof state after:
no goals
Theorem: Probly.Rand.lintegral_bind
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5239
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ ∫⁻ (x' : Y), φ x' ∂↑(bind x f).μ = ∫⁻ (x' : X), ∫⁻ (y' : Y), φ y' ∂↑(f x').μ ∂↑x.μ
Tactic:
simp [bind]
Proof state after:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5239
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ (∫⁻ (x' : Y), φ x' ∂Measure.bind ↑x.μ fun x => ↑(f x).μ) = ∫⁻ (x' : X), ∫⁻ (x' : Y), φ x' ∂↑(f x').μ ∂↑x.μ
Theorem: Probly.Rand.lintegral_bind
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5239
inst✝ : MeasurableSpace Z
x : Rand X
f : X → Rand Y
φ : Y → ℝ≥0∞
hf : Measurable f
hφ : Measurable φ
⊢ (∫⁻ (x' : Y), φ x' ∂Measure.bind ↑x.μ fun x => ↑(f x).μ) = ∫⁻ (x' : X), ∫⁻ (x' : Y), φ x' ∂↑(f x').μ ∂↑x.μ
Tactic:
apply Measure.lintegral_bind (is_measurable hf) hφ
Proof state after:
no goals
Theorem: Probly.Rand.bind_bind
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
⊢ bind (bind x g) f = bind x fun x' => bind (g x') f
Tactic:
ext
Proof state after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (bind x g) f).μ s✝ = ↑↑↑(bind x fun x' => bind (g x') f).μ s✝
Theorem: Probly.Rand.bind_bind
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (bind x g) f).μ s✝ = ↑↑↑(bind x fun x' => bind (g x') f).μ s✝
Tactic:
simp [bind]
Proof state after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.bind ↑x.μ fun x => ↑(g x).μ) fun x => ↑(f x).μ) s✝ =
    ↑↑(Measure.bind ↑x.μ fun x => Measure.bind ↑(g x).μ fun x => ↑(f x).μ) s✝
Theorem: Probly.Rand.bind_bind
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type
inst✝ : MeasurableSpace Z
x : Rand X
g : X → Rand Y
f : Y → Rand Z
hg : Measurable g
hf : Measurable f
s✝ : Set Z
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.bind ↑x.μ fun x => ↑(g x).μ) fun x => ↑(f x).μ) s✝ =
    ↑↑(Measure.bind ↑x.μ fun x => Measure.bind ↑(g x).μ fun x => ↑(f x).μ) s✝
Tactic:
rw[Measure.bind_bind (m:=x.μ) (is_measurable hg) (is_measurable hf)]
Proof state after:
no goals
Theorem: Probly.Rand.bind_pure
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.13258
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
⊢ bind (pure x) f = f x
Tactic:
ext
Proof state after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.13258
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
s✝ : Set Y
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (pure x) f).μ s✝ = ↑↑↑(f x).μ s✝
Theorem: Probly.Rand.bind_pure
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.13258
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
s✝ : Set Y
a✝ : MeasurableSet s✝
⊢ ↑↑↑(bind (pure x) f).μ s✝ = ↑↑↑(f x).μ s✝
Tactic:
simp[bind,pure]
Proof state after:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.13258
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
s✝ : Set Y
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.dirac x) fun x => ↑(f x).μ) s✝ = ↑↑↑(f x).μ s✝
Theorem: Probly.Rand.bind_pure
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.13258
inst✝ : MeasurableSpace Z
f : X → Rand Y
hf : Measurable f
x : X
s✝ : Set Y
a✝ : MeasurableSet s✝
⊢ ↑↑(Measure.bind (Measure.dirac x) fun x => ↑(f x).μ) s✝ = ↑↑↑(f x).μ s✝
Tactic:
rw[Measure.bind_dirac (is_measurable hf) x]
Proof state after:
no goals
Theorem: Probly.Rand.pure_E
Proof state before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.21067
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : X
φ : X → Y
⊢ E (pure x) φ = φ x
Tactic:
simp (disch:=sorry) only [E,expectedValue,rand_simp]
Proof state after:
no goals
Theorem: Probly.Rand.bind_E
Proof state before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type
inst✝⁷ : MeasurableSpace Y
Z : Type u_1
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : Rand X
f : X → Rand Y
φ : Y → Z
⊢ E (bind x f) φ = E x fun x' => E (f x') φ
Tactic:
simp (disch:=sorry) only [E,expectedValue,rand_simp]
Proof state after:
no goals
Theorem: Probly.Rand.zero_E
Proof state before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.22558
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : Rand X
⊢ (E x fun x => 0) = 0
Tactic:
simp only [E,expectedValue,integral_zero]
Proof state after:
no goals
Theorem: Probly.Rand.expectedValue_smul
Proof state before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.23797
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : Rand X
φ : X → ℝ
y : Y
⊢ (E x fun x' => φ x' • y) = E x φ • y
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.Rand.expectedValue_as_mean
Proof state before:
X : Type
inst✝⁸ : MeasurableSpace X
Y : Type
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.27192
inst✝⁶ : MeasurableSpace Z
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace ℝ X
inst✝³ : NormedAddCommGroup Y
inst✝² : NormedSpace ℝ Y
inst✝¹ : NormedAddCommGroup Z
inst✝ : NormedSpace ℝ Z
x : Rand X
φ : X → Y
hφ : Measurable φ
⊢ E x φ =
    mean
      (let x' ~ x
      pure (φ x'))
Tactic:
simp (disch:=sorry) [mean,expectedValue,E,hφ]
Proof state after:
no goals
Theorem: Probly.Rand.bind_pdf
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ pdf' (bind x f) ν = fun y => ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ
Tactic:
funext y
Proof state after:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf' (bind x f) ν y = ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ
Theorem: Probly.Rand.bind_pdf
Proof state before:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf' (bind x f) ν y = ∫ (x' : X), pdf' (f x') ν y ∂↑x.μ
Tactic:
simp[Rand.pdf',Rand.bind,Rand.pure]
Proof state after:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ ENNReal.toReal (Measure.rnDeriv (Measure.bind ↑x.μ fun x => ↑(f x).μ) ν y) =
    ∫ (x' : X), ENNReal.toReal (Measure.rnDeriv (↑(f x').μ) ν y) ∂↑x.μ
Theorem: Probly.Rand.bind_pdf
Proof state before:
case h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.33450
inst✝ : MeasurableSpace Z
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ ENNReal.toReal (Measure.rnDeriv (Measure.bind ↑x.μ fun x => ↑(f x).μ) ν y) =
    ∫ (x' : X), ENNReal.toReal (Measure.rnDeriv (↑(f x').μ) ν y) ∂↑x.μ
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.dnormal.density_wrt_normal
Proof state before:
μ σ dμ dσ : ℝ
⊢ DRand.density (dnormal μ σ dμ dσ) ↑(normal μ σ).μ = fun x =>
    (dμ * (x - μ) + dσ * (x - μ - σ) * (x - μ + σ) / σ) / σ ^ 2
Tactic:
sorry
Proof state after:
no goals
Theorem: Probly.randFwdDeriv_const
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.604
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.721
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.838
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.961
inst✝ : MeasurableSpace β
a : Rand α
⊢ (randFwdDeriv fun x => a) = fun x x => { val := a, dval := 0 }
Tactic:
unfold randFwdDeriv
Proof state after:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.604
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.721
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.838
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.961
inst✝ : MeasurableSpace β
a : Rand α
⊢ (fun x dx => { val := (fun x => a) x, dval := randDeriv (fun x => a) x dx }) = fun x x => { val := a, dval := 0 }
Theorem: Probly.randFwdDeriv_const
Proof state before:
W : Type u_1
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type ?u.604
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type ?u.721
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type ?u.838
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type
inst✝¹ : MeasurableSpace α
β : Type ?u.961
inst✝ : MeasurableSpace β
a : Rand α
⊢ (fun x dx => { val := (fun x => a) x, dval := randDeriv (fun x => a) x dx }) = fun x x => { val := a, dval := 0 }
Tactic:
simp only [rand_simp]
Proof state after:
no goals
Theorem: Probly.randFwdDeriv_comp
Proof state before:
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
⊢ (randFwdDeriv fun x => f (g x)) = fun x dx =>
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2
Tactic:
funext x dx
Proof state after:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randFwdDeriv (fun x => f (g x)) x dx =
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2
Theorem: Probly.randFwdDeriv_comp
Proof state before:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randFwdDeriv (fun x => f (g x)) x dx =
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2
Tactic:
unfold randFwdDeriv fwdDeriv
Proof state after:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ { val := (fun x => f (g x)) x, dval := randDeriv (fun x => f (g x)) x dx } =
    let ydy := (g x, (fderiv ℝ g x) dx);
    { val := f ydy.1, dval := randDeriv f ydy.1 ydy.2 }
Theorem: Probly.randFwdDeriv_comp
Proof state before:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ { val := (fun x => f (g x)) x, dval := randDeriv (fun x => f (g x)) x dx } =
    let ydy := (g x, (fderiv ℝ g x) dx);
    { val := f ydy.1, dval := randDeriv f ydy.1 ydy.2 }
Tactic:
simp (disch := first | apply hf | apply hg) only [rand_simp,randDeriv_comp]
Proof state after:
no goals
Theorem: Probly.FDRand.pure.arg_x.randFwdDeriv_rule
Proof state before:
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
⊢ (randFwdDeriv fun w => Rand.pure (x w)) = fun w dw => fdpure (x w) ((fderiv ℝ x w) dw)
Tactic:
unfold randFwdDeriv fdpure
Proof state after:
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
⊢ (fun x_1 dx => { val := (fun w => Rand.pure (x w)) x_1, dval := randDeriv (fun w => Rand.pure (x w)) x_1 dx }) =
    fun 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:
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
⊢ (fun x_1 dx => { val := (fun w => Rand.pure (x w)) x_1, dval := randDeriv (fun w => Rand.pure (x w)) x_1 dx }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x w) dw) }
Tactic:
simp (disch:=first | apply hx | sorry) only [rand_simp]
Proof state after:
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
⊢ (fun x_1 dx =>
      { val := Rand.pure (x x_1), dval := randDeriv Rand.pure (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun 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:
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
⊢ (fun x_1 dx =>
      { val := Rand.pure (x x_1), dval := randDeriv Rand.pure (x x_1) ((fderiv ℝ (fun x_2 => x x_2) x_1) dx) }) =
    fun w dw => { val := Rand.pure (x w), dval := dpure (x w) ((fderiv ℝ x 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
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) }