internlm/Lean-Github huggingface dataset:
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
⊢ (Nat.recOn Nat.zero x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn Nat.zero (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
Tactic:
simp[mean]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (Nat.recOn (Nat.succ n) x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn (Nat.succ n) (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
Tactic:
simp[hn,mean,map]
Proof state after:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (r n).𝔼
      (f n
        ((Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).𝔼
          id)) =
    (do
          let x' ←
            Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n
          let y' ← r n
          pure (f n x' y')).𝔼
      id
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (r n).𝔼
      (f n
        ((Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).𝔼
          id)) =
    (do
          let x' ←
            Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n
          let y' ← r n
          pure (f n x' y')).𝔼
      id
Tactic:
conv => simp[rand_pull_E,map]
Proof state after:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (mean do
      let x' ← r n
      pure
          (f n
            (mean
              (Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n))
            x')) =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (mean do
      let x' ← r n
      pure
          ((Nat.rec (pure x₀)
                (fun n x => do
                  let x' ← x
                  let y' ← r n
                  pure (f n x' y'))
                n).𝔼
            fun x => f n x x')) =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Tactic:
conv =>
  simp[rand_pull_E]
Proof state after:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (mean do
      let x' ← r n
      (Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).map
          fun x => f n x x') =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Theorem: SciLean.Rand.pull_E_nat_recOn
Proof state before:
R : Type ?u.59471
inst✝¹³ : RealScalar R
X : Type ?u.59474
inst✝¹² : MeasurableSpace X
inst✝¹¹ : AddCommGroup X
inst✝¹⁰ : Module ℝ X
Y : Type ?u.60079
inst✝⁹ : AddCommGroup Y
inst✝⁸ : Module ℝ Y
inst✝⁷ : MeasurableSpace Y
Z : Type ?u.60683
inst✝⁶ : AddCommGroup Z
inst✝⁵ : Module ℝ Z
C : ℕ → Type
inst✝⁴ : (n : ℕ) → AddCommGroup (C n)
inst✝³ : (n : ℕ) → Module ℝ (C n)
inst✝² : (n : ℕ) → MeasurableSpace (C n)
D : ℕ → Type
inst✝¹ inst✝ : (n : ℕ) → MeasurableSpace (D n)
x₀ : C 0
r : (n : ℕ) → Rand (D n)
f : (n : ℕ) → C n → D n → C (n + 1)
hf : ∀ (n : ℕ) (d : D n), IsAffineMap ℝ fun x => f n x d
n : ℕ
hn :
  (Nat.recOn n x₀ fun n x => (r n).𝔼 (f n x)) =
    mean
      (Nat.recOn n (pure x₀) fun n x => do
        let x' ← x
        let y' ← r n
        pure (f n x' y'))
⊢ (mean do
      let x' ← r n
      (Nat.rec (pure x₀)
              (fun n x => do
                let x' ← x
                let y' ← r n
                pure (f n x' y'))
              n).map
          fun x => f n x x') =
    mean do
      let x' ←
        Nat.rec (pure x₀)
            (fun n x => do
              let x' ← x
              let y' ← r n
              pure (f n x' y'))
            n
      let y' ← r n
      pure (f n x' y')
Tactic:
rw[Rand.swap_bind]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_list_recOn
Proof state before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn [] x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn [] (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
case nil => simp[mean]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_list_recOn
Proof state before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
⊢ (List.recOn [] x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn [] (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
simp[mean]
Proof state after:
no goals
Theorem: SciLean.Rand.pull_E_list_recOn
Proof state before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (List.recOn (head :: tail) x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn (head :: tail) (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
Tactic:
simp[hn,mean]
Proof state after:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (r head tail).𝔼
      (f head tail
        ((List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).𝔼
          id)) =
    (do
          let x' ←
            List.rec (pure x₀)
                (fun head tail x => do
                  let x' ← x
                  let y' ← r head tail
                  pure (f head tail x' y'))
                tail
          let y' ← r head tail
          pure (f head tail x' y')).𝔼
      id
Theorem: SciLean.Rand.pull_E_list_recOn
Proof state before:
R : Type ?u.82718
inst✝¹² : RealScalar R
X : Type ?u.82721
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : AddCommGroup X
inst✝⁹ : Module ℝ X
Y : Type ?u.83326
inst✝⁸ : AddCommGroup Y
inst✝⁷ : Module ℝ Y
inst✝⁶ : MeasurableSpace Y
Z : Type ?u.83930
inst✝⁵ : AddCommGroup Z
inst✝⁴ : Module ℝ Z
α : Type u_1
C : List α → Type
inst✝³ : (n : List α) → AddCommGroup (C n)
inst✝² : (n : List α) → Module ℝ (C n)
inst✝¹ : (n : List α) → MeasurableSpace (C n)
D : List α → Type
inst✝ : (n : List α) → MeasurableSpace (D n)
x₀ : C []
r : (head : α) → (tail : List α) → Rand (D (head :: tail))
f : (head : α) → (tail : List α) → C tail → D (head :: tail) → C (head :: tail)
hf : ∀ (head : α) (tail : List α) (d : D (head :: tail)), IsAffineMap ℝ fun x => f head tail x d
head : α
tail : List α
hn :
  (List.recOn tail x₀ fun head tail x => (r head tail).𝔼 (f head tail x)) =
    mean
      (List.recOn tail (pure x₀) fun head tail x => do
        let x' ← x
        let y' ← r head tail
        pure (f head tail x' y'))
⊢ (mean do
      let x' ← r head tail
      (List.rec (pure x₀)
              (fun head tail x => do
                let x' ← x
                let y' ← r head tail
                pure (f head tail x' y'))
              tail).map
          fun x => f head tail x x') =
    mean do
      let x' ←
        List.rec (pure x₀)
            (fun head tail x => do
              let x' ← x
              let y' ← r head tail
              pure (f head tail x' y'))
            tail
      let y' ← r head tail
      pure (f head tail x' y')
Tactic:
rw[Rand.swap_bind]
Proof state after:
no goals
Theorem: SciLean.postExtAction_postComp
Proof state before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => Distribution.extAction' T φ
Tactic:
unfold Distribution.extAction'
Proof state after:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => T.extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Theorem: SciLean.postExtAction_postComp
Proof state before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun T => T.extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.postExtAction_postComp
Proof state before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => Distribution.extAction' (y u) φ
Tactic:
unfold Distribution.extAction'
Proof state after:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => (y u).extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Theorem: SciLean.postExtAction_postComp
Proof state before:
R : Type ?u.21150
inst✝¹⁰ : RealScalar R
X : Type ?u.21156
inst✝⁹ : Vec R X
Y : Type ?u.21186
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type ?u.22048
inst✝⁶ : Vec R Z
U : Type ?u.22072
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ IsSmoothLinearMap R fun u => (y u).extAction φ (fun y ⊸[R] fun r ⊸[R] r • y)
Tactic:
fun_prop
Proof state after:
no goals
Theorem: SciLean.postExtAction_postComp
Proof state before:
R : Type u_1
inst✝¹⁰ : RealScalar R
X : Type u_2
inst✝⁹ : Vec R X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
U : Type u_3
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ Distribution.postComp (Distribution.postComp x y) (fun T ⊸ Distribution.extAction' T φ) =
    Distribution.postComp x (fun u ⊸ Distribution.extAction' (y u) φ)
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.parDistribFwdDeriv.comp_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (parDistribFwdDeriv fun x => f (g x)) = fun x dx =>
    let ydy := ∂> g x dx;
    parDistribFwdDeriv f ydy.1 ydy.2
Tactic:
unfold parDistribFwdDeriv
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (fun x dx =>
      let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Theorem: SciLean.parDistribFwdDeriv.comp_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (fun x dx =>
      let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Tactic:
funext x dx
Proof state after:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x dx : X
⊢ (let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
    let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
    z + dz) =
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Theorem: SciLean.parDistribFwdDeriv.comp_rule
Proof state before:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x dx : X
⊢ (let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
    let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
    z + dz) =
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Tactic:
fun_trans [action_push,fwdDeriv]
Proof state after:
no goals