internlm/Lean-Github huggingface dataset:
Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule
Proof state before:
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
⊢ (fun x =>
      (odeSolve f t₀ t (x₀ x),
        semiAdjoint R fun dw =>
          (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
              (∂> (w:=x;dw), x₀ w)).2)) =
    fun w =>
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
Tactic:
funext w
Proof state after:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (odeSolve f t₀ t (x₀ w),
      semiAdjoint R fun dw =>
        (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
            (∂> (w:=w;dw), x₀ w)).2) =
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule
Proof state before:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (odeSolve f t₀ t (x₀ w),
      semiAdjoint R fun dw =>
        (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
            (∂> (w:=w;dw), x₀ w)).2) =
    (odeSolve f t₀ t (x₀ w), fun dx =>
      semiAdjoint R (∂ x₀ w)
        (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx))
Tactic:
simp
Proof state after:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (semiAdjoint R fun dw =>
      (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
          (∂> (w:=w;dw), x₀ w)).2) =
    fun dx =>
    semiAdjoint R (∂ x₀ w) (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx)
Theorem: SciLean.odeSolve.arg_x₀.revCDeriv_rule
Proof state before:
case h
R✝ : Type ?u.22324
inst✝⁶ : RCLike R✝
X✝ : Type ?u.22330
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : SemiInnerProductSpace R W
X : Type u_2
inst✝² : SemiInnerProductSpace R X
Y : Type ?u.22376
inst✝¹ : SemiInnerProductSpace R Y
Z : Type ?u.22388
inst✝ : SemiInnerProductSpace R Z
f : R → X → X
t₀ t : R
x₀ : W → X
hf :
  HasAdjDiff R fun x =>
    match x with
    | (t, x) => f t x
hx : HasAdjDiff R x₀
w : W
⊢ (semiAdjoint R fun dw =>
      (odeSolve (fun t xdx => ∂> (wkx0wkx1:=(t, xdx.1);(0, xdx.2)), f wkx0wkx1.1 wkx0wkx1.2) t₀ t₀
          (∂> (w:=w;dw), x₀ w)).2) =
    fun dx =>
    semiAdjoint R (∂ x₀ w) (odeSolve (fun s dx' => -semiAdjoint R (∂ (x':=odeSolve f t₀ s (x₀ w)), f s x') dx') t₀ t dx)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.bind_probability
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
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.2329
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: SciLean.Prob.Rand.bind_probability
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.2329
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: SciLean.Prob.Rand.lintegral_bind
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5407
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.5407
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: SciLean.Prob.Rand.lintegral_bind
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.5407
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: SciLean.Prob.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: SciLean.Prob.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: SciLean.Prob.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: SciLean.Prob.Rand.bind_pure
Proof state before:
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.17225
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.17225
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: SciLean.Prob.Rand.bind_pure
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.17225
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.17225
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: SciLean.Prob.Rand.bind_pure
Proof state before:
case a.h.h
X : Type
inst✝² : MeasurableSpace X
Y : Type
inst✝¹ : MeasurableSpace Y
Z : Type ?u.17225
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: SciLean.Prob.Rand.pure_E
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.26205
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.26211
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : X
φ : X → Y
⊢ E (pure x) φ = φ x
Tactic:
simp (disch:=sorry) only [E,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.bind_E
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : MeasurableSpace Y
Z : Type u_1
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.27216
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
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,rand_simp]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.zero_E
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.28409
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.28415
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
⊢ (E x fun x => 0) = 0
Tactic:
simp only [E,integral_zero]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.add_E
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ (E x fun x => φ x + ψ x) = E x φ + E x ψ
Tactic:
simp only [E]
Proof state after:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ ∫ (x' : X), φ x' + ψ x' ∂↑x.μ = ∫ (x' : X), φ x' ∂↑x.μ + ∫ (x' : X), ψ x' ∂↑x.μ
Theorem: SciLean.Prob.Rand.add_E
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.30017
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.30023
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ ψ : X → Y
⊢ ∫ (x' : X), φ x' + ψ x' ∂↑x.μ = ∫ (x' : X), φ x' ∂↑x.μ + ∫ (x' : X), ψ x' ∂↑x.μ
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.expectedValue_smul
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type u_1
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.32631
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.32637
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
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: SciLean.Prob.Rand.expectedValue_as_mean
Proof state before:
X : Type
inst✝¹² : MeasurableSpace X
Y : Type
inst✝¹¹ : MeasurableSpace Y
Z : Type ?u.36867
inst✝¹⁰ : MeasurableSpace Z
R : Type ?u.36873
inst✝⁹ : RealScalar R
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace R X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace R X
inst✝³ : NormedSpace ℝ Y
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace R X
inst✝ : NormedSpace ℝ Z
x : Rand X
φ : X → Y
hφ : Measurable φ
⊢ E x φ =
    mean
      (let x' ~ x
      pure (φ x'))
Tactic:
simp (disch:=sorry) [mean,E,hφ]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.rpdf_wrt_self
Proof state before:
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x : Rand X
⊢ rpdf x ↑x.μ = 1
Tactic:
funext x
Proof state after:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ rpdf x✝ (↑x✝.μ) x = 1 x
Theorem: SciLean.Prob.Rand.rpdf_wrt_self
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ rpdf x✝ (↑x✝.μ) x = 1 x
Tactic:
unfold rpdf
Proof state after:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ pdf ℝ x✝ (↑x✝.μ) x = 1 x
Theorem: SciLean.Prob.Rand.rpdf_wrt_self
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type ?u.44518
inst✝² : MeasurableSpace Y
Z : Type ?u.44524
inst✝¹ : MeasurableSpace Z
R : Type ?u.44530
inst✝ : RealScalar R
x✝ : Rand X
x : X
⊢ pdf ℝ x✝ (↑x✝.μ) x = 1 x
Tactic:
rw[pdf_wrt_self]
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.bind_rpdf
Proof state before:
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ rpdf (bind x f) ν = fun y => ∫ (x' : X), rpdf (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.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf (bind x f) ν y = ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ
Theorem: SciLean.Prob.Rand.bind_rpdf
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf (bind x f) ν y = ∫ (x' : X), rpdf (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.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf
      { μ := erase (Measure.bind ↑x.μ fun x => ↑(f x).μ), is_prob := ⋯,
        rand := do
          let __do_lift ← x.rand
          (f __do_lift).rand }
      ν y =
    ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ
Theorem: SciLean.Prob.Rand.bind_rpdf
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.44890
inst✝¹ : MeasurableSpace Z
R : Type ?u.44896
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ rpdf
      { μ := erase (Measure.bind ↑x.μ fun x => ↑(f x).μ), is_prob := ⋯,
        rand := do
          let __do_lift ← x.rand
          (f __do_lift).rand }
      ν y =
    ∫ (x' : X), rpdf (f x') ν y ∂↑x.μ
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.Prob.Rand.bind_pdf
Proof state before:
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
⊢ pdf R (bind x f) ν = fun y => ∫ (x' : X), pdf R (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.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (bind x f) ν y = ∫ (x' : X), pdf R (f x') ν y ∂↑x.μ
Theorem: SciLean.Prob.Rand.bind_pdf
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ pdf R (bind x f) ν y = ∫ (x' : X), pdf R (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.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R ((Measure.bind ↑x.μ fun x => ↑(f x).μ).rnDeriv ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((↑(f x').μ).rnDeriv ν y).toReal ∂↑x.μ
Theorem: SciLean.Prob.Rand.bind_pdf
Proof state before:
case h
X : Type
inst✝³ : MeasurableSpace X
Y : Type
inst✝² : MeasurableSpace Y
Z : Type ?u.46786
inst✝¹ : MeasurableSpace Z
R : Type u_1
inst✝ : RealScalar R
ν : Measure Y
x : Rand X
f : X → Rand Y
y : Y
⊢ Scalar.ofReal R ((Measure.bind ↑x.μ fun x => ↑(f x).μ).rnDeriv ν y).toReal =
    ∫ (x' : X), Scalar.ofReal R ((↑(f x').μ).rnDeriv ν y).toReal ∂↑x.μ
Tactic:
sorry
Proof state after:
no goals
Theorem: SciLean.ArrayType.ext
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝³ : IndexType Idx
inst✝² : outParam (DecidableEq Idx)
inst✝¹ : LawfulIndexType Idx
inst✝ : ArrayType Cont Idx Elem
x y : Cont
⊢ (∀ (i : Idx), x[i] = y[i]) → x = y
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.ArrayType.add_ofFn
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Add Elem
f g : Idx → Elem
⊢ Indexed.ofFn f + Indexed.ofFn g = Indexed.ofFn fun i => f i + g i
Tactic:
apply ArrayType.ext (Idx:=Idx)
Proof state after:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Add Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f + Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i + g i)[i]
Theorem: SciLean.ArrayType.add_ofFn
Proof state before:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Add Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f + Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i + g i)[i]
Tactic:
simp[HAdd.hAdd, Add.add]
Proof state after:
no goals
Theorem: SciLean.ArrayType.sub_ofFn
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Sub Elem
f g : Idx → Elem
⊢ Indexed.ofFn f - Indexed.ofFn g = Indexed.ofFn fun i => f i - g i
Tactic:
apply ArrayType.ext (Idx:=Idx)
Proof state after:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Sub Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f - Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i - g i)[i]
Theorem: SciLean.ArrayType.sub_ofFn
Proof state before:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Sub Elem
f g : Idx → Elem
⊢ ∀ (i : Idx), (Indexed.ofFn f - Indexed.ofFn g)[i] = (Indexed.ofFn fun i => f i - g i)[i]
Tactic:
simp[HSub.hSub, Sub.sub]
Proof state after:
no goals
Theorem: SciLean.ArrayType.neg_ofFn
Proof state before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
f : Idx → Elem
⊢ -Indexed.ofFn f = Indexed.ofFn fun i => -f i
Tactic:
apply ArrayType.ext (Idx:=Idx)
Proof state after:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
f : Idx → Elem
⊢ ∀ (i : Idx), (-Indexed.ofFn f)[i] = (Indexed.ofFn fun i => -f i)[i]
Theorem: SciLean.ArrayType.neg_ofFn
Proof state before:
case a
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Neg Elem
f : Idx → Elem
⊢ ∀ (i : Idx), (-Indexed.ofFn f)[i] = (Indexed.ofFn fun i => -f i)[i]
Tactic:
simp[Neg.neg]
Proof state after:
no goals
Theorem: SciLean.ArrayType.smul_ofFn
Proof state before:
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ a • Indexed.ofFn f = Indexed.ofFn fun i => a • f i
Tactic:
apply ArrayType.ext (Idx:=Idx)
Proof state after:
case a
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ ∀ (i : Idx), (a • Indexed.ofFn f)[i] = (Indexed.ofFn fun i => a • f i)[i]