internlm/Lean-Github huggingface dataset:
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    let ydg := revDeriv' R g x;
    let udf := parDistribRevDeriv f ydg.1;
    postComp udf (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] ydg.2 (udf'.2 du)))
Tactic:
simp
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    postComp (parDistribRevDeriv f (g x)) (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    postComp (parDistribRevDeriv f (g x)) (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
Tactic:
unfold parDistribRevDeriv postComp
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (fun x =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
        let z := ((fun x => f (g x)) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (fun x =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
        let z := ((fun x => f (g x)) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Tactic:
funext x
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
⊢ (fun φ ⊸
      let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
      let z := ((fun x => f (g x)) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
⊢ (fun φ ⊸
      let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
      let z := ((fun x => f (g x)) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Tactic:
ext φ
Proof state after:
case h.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
⊢ ((fun φ ⊸
          let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
          let z := ((fun x => f (g x)) x) φ;
          (z, fun dz ⊸[R] df' dz))
        φ).1 =
    ((fun φ ⊸[R]
          (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
            ((fun φ ⊸
                let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                let z := (f (g x)) φ;
                (z, fun dz ⊸[R] df' dz))
              φ))
        φ).1

case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
case h.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
⊢ ((fun φ ⊸
          let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
          let z := ((fun x => f (g x)) x) φ;
          (z, fun dz ⊸[R] df' dz))
        φ).1 =
    ((fun φ ⊸[R]
          (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
            ((fun φ ⊸
                let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                let z := (f (g x)) φ;
                (z, fun dz ⊸[R] df' dz))
              φ))
        φ).1

case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Tactic:
simp
Proof state after:
case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Theorem: SciLean.parDistribRevDeriv.comp_rule
Proof state before:
case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.parDistribRevDeriv.bind_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
⊢ (parDistribRevDeriv fun x => Distribution.bind (g x) (f x) L) = fun x =>
    let ydg := parDistribRevDeriv g x;
    let zdf := fun y => parDistribRevDeriv (fun x => f x y) x;
    Distribution.bind ydg zdf
      (fun x ⊸
        match x with
        | (u, dg) =>
          fun vdf ⊸
            ((L u) vdf.1,
              fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw)))
Tactic:
unfold parDistribRevDeriv Distribution.bind
Proof state after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
⊢ (fun x =>
      fun φ ⊸
        let df' :=
          semiAdjoint R fun dx =>
            ∂ (x:=x;dx), ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    let ydg :=
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
        let z := (g x) φ;
        (z, fun dz ⊸[R] df' dz);
    let zdf := fun y =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
        let z := ((fun x => f x y) x) φ;
        (z, fun dz ⊸[R] df' dz);
    fun φ ⊸[R]
      ⟪ydg, fun x =>
        ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
          match x with
          | (u, dg) =>
            fun vdf ⊸
              ((L u) vdf.1,
                fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))]
Theorem: SciLean.parDistribRevDeriv.bind_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
⊢ (fun x =>
      fun φ ⊸
        let df' :=
          semiAdjoint R fun dx =>
            ∂ (x:=x;dx), ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    let ydg :=
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
        let z := (g x) φ;
        (z, fun dz ⊸[R] df' dz);
    let zdf := fun y =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
        let z := ((fun x => f x y) x) φ;
        (z, fun dz ⊸[R] df' dz);
    fun φ ⊸[R]
      ⟪ydg, fun x =>
        ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
          match x with
          | (u, dg) =>
            fun vdf ⊸
              ((L u) vdf.1,
                fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))]
Tactic:
funext x
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
x : X
⊢ (fun φ ⊸
      let df' :=
        semiAdjoint R fun dx =>
          ∂ (x:=x;dx), ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
      let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    let ydg :=
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
        let z := (g x) φ;
        (z, fun dz ⊸[R] df' dz);
    let zdf := fun y =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
        let z := ((fun x => f x y) x) φ;
        (z, fun dz ⊸[R] df' dz);
    fun φ ⊸[R]
      ⟪ydg, fun x =>
        ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
          match x with
          | (u, dg) =>
            fun vdf ⊸
              ((L u) vdf.1,
                fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))]
Theorem: SciLean.parDistribRevDeriv.bind_rule
Proof state before:
case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
x : X
φ : 𝒟 Z
x✝ : W
⊢ ((fun φ ⊸
            let df' :=
              semiAdjoint R fun dx =>
                ∂ (x:=x;dx),
                  ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
            let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((let ydg :=
            fun φ ⊸
              let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
              let z := (g x) φ;
              (z, fun dz ⊸[R] df' dz);
          let zdf := fun y =>
            fun φ ⊸
              let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
              let z := ((fun x => f x y) x) φ;
              (z, fun dz ⊸[R] df' dz);
          fun φ ⊸[R]
            ⟪ydg, fun x =>
              ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
                match x with
                | (u, dg) =>
                  fun vdf ⊸
                    ((L u) vdf.1,
                      fun dw ⊸[R]
                        vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))])
          φ).2
      x✝
Tactic:
sorry_proof
Proof state after:
no goals
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
⊢ (parDistribRevDeriv fun w => dirac (x w)) = fun w =>
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
Tactic:
funext w
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ parDistribRevDeriv (fun w => dirac (x w)) w =
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ parDistribRevDeriv (fun w => dirac (x w)) w =
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
Tactic:
apply Distribution.ext _ _
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ ∀ (φ : 𝒟 X),
    (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
      (let xdx := revDeriv' R x w;
        postComp (diracRevDeriv xdx.1)
          (fun x ⊸
            match x with
            | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
        φ
Theorem: SciLean.parDistribRevDeriv.dirac.arg_xy.parDistribRevDeriv_rule
Proof state before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ ∀ (φ : 𝒟 X),
    (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
      (let xdx := revDeriv' R x w;
        postComp (diracRevDeriv xdx.1)
          (fun x ⊸
            match x with
            | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
        φ
Tactic:
intro φ
Proof state after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
φ : 𝒟 X
⊢ (parDistribRevDeriv (fun w => dirac (x w)) w) φ =
    (let xdx := revDeriv' R x w;
      postComp (diracRevDeriv xdx.1)
        (fun x ⊸
          match x with
          | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr))))
      φ