From db9a9f94aab5c642488119fc74947258a1d88617 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Wed, 22 Nov 2023 18:27:31 -0500 Subject: [PATCH] basic rules for revDerivProj(Update) --- .../FunctionTransformations/RevCDeriv.lean | 7 + .../FunctionTransformations/RevDerivProj.lean | 623 +++++++++++++++--- .../RevDerivUpdate.lean | 14 +- SciLean/Data/StructLike/Algebra.lean | 12 +- SciLean/Data/StructLike/Basic.lean | 2 +- 5 files changed, 579 insertions(+), 79 deletions(-) diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean index 6e879ad6..ee8be755 100644 --- a/SciLean/Core/FunctionTransformations/RevCDeriv.lean +++ b/SciLean/Core/FunctionTransformations/RevCDeriv.lean @@ -50,6 +50,13 @@ theorem revCDeriv_fst (f : X → Y) (x : X) by rfl +@[simp, ftrans_simp] +theorem revCDeriv_snd_zero (f : X → Y) (x : X) + : (revCDeriv K f x).2 0 = 0 := +by + simp[revCDeriv] + + @[ftrans] theorem semiAdjoint.arg_a3.cderiv_rule (f : X → Y) (a0 : W → Y) (ha0 : IsDifferentiable K a0) diff --git a/SciLean/Core/FunctionTransformations/RevDerivProj.lean b/SciLean/Core/FunctionTransformations/RevDerivProj.lean index b5b828a5..a5c3bd30 100644 --- a/SciLean/Core/FunctionTransformations/RevDerivProj.lean +++ b/SciLean/Core/FunctionTransformations/RevDerivProj.lean @@ -22,6 +22,7 @@ variable [SemiInnerProductSpace K F] [∀ j, SemiInnerProductSpace K (FJ j)] [SemiInnerProductSpaceStruct K F J FJ] + noncomputable def revDerivProj (f : X → E) (x : X) : E×((i : I)→EI i→X) := @@ -37,19 +38,42 @@ def revDerivProjUpdate (ydf'.1, fun i de dx => dx + ydf'.2 i de) - @[simp, ftrans_simp] theorem revDerivProj_fst (f : X → E) (x : X) : (revDerivProj K f x).1 = f x := by rfl +@[simp, ftrans_simp] +theorem revDerivProj_snd_zero (f : X → E) (x : X) (i : I) + : (revDerivProj K f x).2 i 0 = 0 := +by + simp[revDerivProj] + conv in (StructLike.make _) => + equals (0:E) => + apply StructLike.ext + intro i'; simp + if h : i=i' then subst h; simp else simp[h] + simp + @[simp, ftrans_simp] theorem revDerivProjUpdate_fst (f : X → E) (x : X) : (revDerivProjUpdate K f x).1 = f x := by rfl +@[simp, ftrans_simp] +theorem revDerivProjUpdate_snd_zero (f : X → E) (x dx : X) (i : I) + : (revDerivProjUpdate K f x).2 i 0 dx = dx := +by + simp[revDerivProjUpdate] + +@[simp, ftrans_simp] +theorem revDerivProjUpdate_snd_zero' (f : X → Y) (x : X) (dy : Y) + : (revDerivUpdate K f x).2 dy 0 = (revCDeriv K f x).2 dy := +by + simp[revDerivUpdate] + -------------------------------------------------------------------------------- @@ -182,6 +206,7 @@ theorem revDerivProj.comp_rule by simp[revDerivProj] ftrans + rfl theorem revDerivProjUpdate.comp_rule @@ -198,15 +223,7 @@ theorem revDerivProjUpdate.comp_rule by funext x simp[revDerivProjUpdate,revDerivProj.comp_rule _ _ _ hf hg] - constructor - . sorry - . - funext i de dx - if h :i=i' then - subst h; simp - else - simp[h] - + rfl theorem revDerivProj.let_rule (f : X → Y → E) (g : X → Y) @@ -219,10 +236,11 @@ theorem revDerivProj.let_rule (zdf'.1, fun i dei => let dxy := zdf'.2 i dei - ydg'.2 dxy.2 1 dxy.1) := + ydg'.2 dxy.2 dxy.1) := by - sorry_proof - + unfold revDerivProj + ftrans + rfl theorem revDerivProjUpdate.let_rule (f : X → Y → E) (g : X → Y) @@ -235,28 +253,46 @@ theorem revDerivProjUpdate.let_rule (zdf'.1, fun i dei dx => let dxy := zdf'.2 i dei (dx,0) - ydg'.2 dxy.2 1 dxy.1) := + ydg'.2 dxy.2 dxy.1) := by - sorry_proof + unfold revDerivProjUpdate + simp [revDerivProj.let_rule _ _ _ hf hg,add_assoc,add_comm,revDerivUpdate] theorem revDerivProj.pi_rule - (f : X → ι → E) (hf : ∀ i, HasAdjDiff K (f · i)) - : (revDerivProj K fun (x : X) (i : ι) => f x i) + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (f · i)) + : (@revDerivProj K _ _ _ _ Unit (fun _ => ι→Y) (instStrucLikeDefault) _ _ fun (x : X) (i : ι) => f x i) = - revDerivProj K fun x => f x := by rfl + fun x => + let ydf := revDerivProjUpdate K f x + (fun i => ydf.1 i, + fun _ df => Id.run do + let mut dx : X := 0 + for i in fullRange ι do + dx := ydf.2 (i,()) (df i) dx + dx) := +by + sorry_proof theorem revDerivProjUpdate.pi_rule - (f : X → ι → E) (hf : ∀ i, HasAdjDiff K (f · i)) - : (revDerivProjUpdate K fun (x : X) (i : ι) => f x i) + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (f · i)) + : (@revDerivProjUpdate K _ _ _ _ Unit (fun _ => ι→Y) (StructLike.instStructLikeDefault) _ _ fun (x : X) (i : ι) => f x i) = - revDerivProjUpdate K fun x => f x := by rfl + fun x => + let ydf := revDerivProjUpdate K f x + (fun i => ydf.1 i, + fun _ df dx => Id.run do + let mut dx : X := dx + for i in fullRange ι do + dx := ydf.2 (i,()) (df i) dx + dx) := +by + sorry_proof -------------------------------------------------------------------------------- - -- Register `revDerivProj` as function transformation -------------------------- -------------------------------------------------------------------------------- @@ -301,8 +337,11 @@ def ftransExt : FTransExt where idRule e X := do let .some K := e.getArg? 0 | return none + IO.println "hih" + let proof ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none] + IO.println s!"proof of {← inferType proof}" tryTheorems - #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ] + #[ { proof := ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none], origin := .decl ``id_rule, rfl := false} ] discharger e constRule e X y := do @@ -387,8 +426,11 @@ def ftransExt : FTransExt where idRule e X := do let .some K := e.getArg? 0 | return none + IO.println "hih" + let proof ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none,none,none] + IO.println s!"proof of {← inferType proof}" tryTheorems - #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ] + #[ { proof := ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none,none,none], origin := .decl ``id_rule, rfl := false} ] discharger e constRule e X y := do @@ -434,44 +476,22 @@ end revDerivProjUpdate -------------------------------------------------------------------------------- - - - -------------------------------------------------------------------------------- + end SciLean open SciLean variable {K : Type _} [IsROrC K] - {X Xi : Type} {XI : Xi → Type} [StructLike X Xi XI] [DecidableEq Xi] - {Y Yi : Type} {YI : Yi → Type} [StructLike Y Yi YI] [DecidableEq Yi] - {Z Zi : Type} {ZI : Zi → Type} [StructLike Z Zi ZI] [DecidableEq Zi] - [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] - [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)] - [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)] + {X Xi : Type _} {XI : Xi → Type _} [StructLike X Xi XI] [EnumType Xi] + {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi] + {Z Zi : Type _} {ZI : Zi → Type _} [StructLike Z Zi ZI] [EnumType Zi] + [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] [SemiInnerProductSpaceStruct K X Xi XI] + [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI] + [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)] [SemiInnerProductSpaceStruct K Z Zi ZI] {W : Type _} [SemiInnerProductSpace K W] {ι : Type _} [EnumType ι] -@[simp] -theorem StruckLike.make_zero - {X I : Type} {XI : I → Type} [StructLike X I XI] - [Zero X] [∀ i, Zero (XI i)] - : StructLike.make (E:=X) (fun _ => 0) - = - 0 := -by - sorry - -@[simp] -theorem revCDeriv_snd_zero - (f : X → Y) (x : X) - : (revCDeriv K f x).2 0 = 0 := sorry - -@[simp] -theorem revDerivUpdate_snd_zero - (f : X → Y) (x : X) - : (revDerivUpdate K f x).2 0 k dy = dy := sorry - -- Prod.mk --------------------------------------------------------------------- -------------------------------------------------------------------------------- @@ -501,6 +521,7 @@ by subst h; rfl } + @[ftrans] theorem Prod.mk.arg_fstsnd.revDerivProjUpdate_rule (g : X → Y) (f : X → Z) @@ -519,13 +540,11 @@ by unfold revDerivProjUpdate funext x; ftrans; simp funext i de dx - induction i <;> - { simp[StructLike.make] - sorry_proof - } + induction i <;> simp ------------------------- +-- Prod.fst -------------------------------------------------------------------- +-------------------------------------------------------------------------------- @[ftrans] theorem Prod.fst.arg_self.revDerivProj_rule @@ -557,35 +576,487 @@ theorem Prod.fst.arg_self.revDerivProjUpdate_rule by unfold revDerivProjUpdate funext x; ftrans; simp - funext e dxy dw - simp[StructLike.make] - -- apply congr_arg -- this fails for some reason :( - -- congr; funext i; congr; funext h; subst h; rfl - sorry_proof - +-- Prod.fst -------------------------------------------------------------------- +-------------------------------------------------------------------------------- -theorem Prod.fst.arg_self.revDeriv_rule +@[ftrans] +theorem Prod.snd.arg_self.revDerivProj_rule (f : W → X×Y) (hf : HasAdjDiff K f) - : revCDeriv K (fun w => (f w).1) + : revDerivProj K (fun x => (f x).2) = fun w => - let xydf' := revDerivProj K f w - (xydf'.1.1, fun dx => xydf'.2 (.inl ()) dx) := + let xydf := revDerivProj K f w + (xydf.1.2, + fun i dxy => xydf.2 (.inr i) dxy) := by - sorry_proof + unfold revDerivProj + funext x; ftrans; simp + funext e dxy + simp[StructLike.make] + apply congr_arg + congr; funext i; congr; funext h; subst h; rfl -theorem Prod.fst.arg_self.revDerivProj_rule - {X I : Type _} {XI : I → Type _} - [StructLike X I XI] [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] +@[ftrans] +theorem Prod.snd.arg_self.revDerivProjUpdate_rule (f : W → X×Y) (hf : HasAdjDiff K f) - : revDerivProj K (fun w => (f w).1) + : revDerivProjUpdate K (fun x => (f x).2) = fun w => - let xydf' := revDerivProj K f w - (xydf'.1.1, - fun i dx => xydf'.2 (.inl i) dx) := + let xydf := revDerivProjUpdate K f w + (xydf.1.2, + fun i dxy dw => xydf.2 (.inr i) dxy dw) := +by + unfold revDerivProjUpdate + funext x; ftrans; simp + + + +-- HAdd.hAdd ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem HAdd.hAdd.arg_a0a1.revDerivProj_rule + (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProj K fun x => f x + g x) + = + fun x => + let ydf := revDerivProj K f x + let ydg := revDerivProjUpdate K g x + (ydf.1 + ydg.1, + fun i dy => (ydg.2 i dy (ydf.2 i dy))) := +by + unfold revDerivProjUpdate; unfold revDerivProj + ftrans + + +@[ftrans] +theorem HAdd.hAdd.arg_a0a1.revDerivProjUpdate_rule + (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProjUpdate K fun x => f x + g x) + = + fun x => + let ydf := revDerivProjUpdate K f x + let ydg := revDerivProjUpdate K g x + (ydf.1 + ydg.1, fun i dy dx => ydg.2 i dy (ydf.2 i dy dx)) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivProjUpdate, add_assoc] + + +-- HSub.hSub ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem HSub.hSub.arg_a0a1.revDerivProj_rule + (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProj K fun x => f x - g x) + = + fun x => + let ydf := revDerivProj K f x + let ydg := revDerivProjUpdate K g x + (ydf.1 - ydg.1, + fun i dy => (ydg.2 i (-dy) (ydf.2 i dy))) := +by + unfold revDerivProjUpdate; unfold revDerivProj + ftrans; simp; sorry_proof -- pulling the minus out is just tedious ... + + +@[ftrans] +theorem HSub.hSub.arg_a0a1.revDerivProjUpdate_rule + (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProjUpdate K fun x => f x - g x) + = + fun x => + let ydf := revDerivProjUpdate K f x + let ydg := revDerivProjUpdate K g x + (ydf.1 - ydg.1, fun i dy dx => ydg.2 i (-dy) (ydf.2 i dy dx)) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivProjUpdate, add_assoc] + + +-- Neg.neg --------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem Neg.neg.arg_a0.revDerivProj_rule + (f : X → Y) + : (revDerivProj K fun x => - f x) + = + fun x => + let ydf := revDerivProj K f x + (-ydf.1, fun i dy => ydf.2 i (-dy)) := +by + unfold revDerivProj; ftrans; simp; sorry_proof -- pulling the minus out is just tedious ... + +@[ftrans] +theorem Neg.neg.arg_a0.revDerivProjUpdate_rule + (f : X → Y) + : (revDerivProjUpdate K fun x => - f x) + = + fun x => + let ydf := revDerivProjUpdate K f x + (-ydf.1, fun i dy dx => ydf.2 i (-dy) dx) := +by + unfold revDerivProjUpdate; ftrans + + +-- HMul.hmul ------------------------------------------------------------------- +-------------------------------------------------------------------------------- +open ComplexConjugate + +@[ftrans] +theorem HMul.hMul.arg_a0a1.revDerivProj_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProj K fun x => f x * g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revCDeriv K g x + (ydf.1 * zdg.1, fun _ dy => ydf.2 ((conj zdg.1)*dy) (zdg.2 (conj ydf.1* dy))) := +by + unfold revDerivProj + ftrans; funext x; simp[revDerivUpdate,StructLike.make]; funext _ dy + sorry_proof -- just need to pull those multiplcations out + + +@[ftrans] +theorem HMul.hMul.arg_a0a1.revDerivProjUpdate_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProjUpdate K fun x => f x * g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivUpdate K g x + (ydf.1 * zdg.1, fun _ dy dx => ydf.2 ((conj zdg.1)*dy) (zdg.2 (conj ydf.1* dy) dx)) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivUpdate,add_assoc] + + +-- SMul.smul ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem HSMul.hSMul.arg_a0a1.revDerivProj_rule + {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi] + [SemiHilbert K Y] [∀ i, SemiHilbert K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI] + (f : X → K) (g : X → Y) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProj K fun x => f x • g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivProj K g x + (ydf.1 • zdg.1, fun i (dy : YI i) => ydf.2 (inner (StructLike.proj zdg.1 i) dy) (zdg.2 i (conj ydf.1•dy))) := +by + unfold revDerivProj + ftrans; funext x; simp; funext i dy + simp[revDerivUpdate] + sorry_proof -- this requires some lemma about inner product with StruckLike types + +@[ftrans] +theorem HSMul.hSMul.arg_a0a1.revDerivProjUpdate_rule + {Y Yi : Type} {YI : Yi → Type} [StructLike Y Yi YI] [EnumType Yi] + [SemiHilbert K Y] [∀ i, SemiHilbert K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI] + (f : X → K) (g : X → Y) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) + : (revDerivProjUpdate K fun x => f x • g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivProjUpdate K g x + (ydf.1 • zdg.1, fun i (dy : YI i) dx => ydf.2 (inner (StructLike.proj zdg.1 i) dy) (zdg.2 i (conj ydf.1•dy) dx)) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivUpdate]; funext x; simp; funext i dy dx + simp[add_assoc] + + + +-- HDiv.hDiv ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDerivProj_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDerivProj K fun x => f x / g x) + = + fun x => + let ydf := revCDeriv K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + -- fun dy k dx => (1 / (conj zdg.1)^2) • (conj zdg.1 • ydf.2 dy - conj ydf.1 • zdg.2 dy)) := + fun _ dy => + let factor := ((conj zdg.1)^2)⁻¹ + let dy := factor * dy + zdg.2 (-conj ydf.1 * dy) (ydf.2 (conj zdg.1 * dy))) := +by + sorry_proof + +@[ftrans] +theorem HDiv.hDiv.arg_a0a1.revDerivProjUpdate_rule + (f g : X → K) + (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0) + : (revDerivProjUpdate K fun x => f x / g x) + = + fun x => + let ydf := revDerivUpdate K f x + let zdg := revDerivUpdate K g x + (ydf.1 / zdg.1, + fun _ dy dx => + let factor := ((conj zdg.1)^2)⁻¹ + let dy := factor * dy + zdg.2 (-conj ydf.1 * dy) (ydf.2 (conj zdg.1 * dy) dx)) := +by + sorry_proof + + +-- HPow.hPow ------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +def HPow.hPow.arg_a0.revDerivProj_rule + (f : X → K) (n : Nat) (hf : HasAdjDiff K f) + : revDerivProj K (fun x => f x ^ n) + = + fun x => + let ydf := revCDeriv K f x + (ydf.1 ^ n, + fun _ dy => ydf.2 (n * (conj ydf.1 ^ (n-1)) * dy)) := +by + sorry_proof + + +@[ftrans] +def HPow.hPow.arg_a0.revDerivProjUpdate_rule + (f : X → K) (n : Nat) (hf : HasAdjDiff K f) + : revDerivProjUpdate K (fun x => f x ^ n) + = + fun x => + let ydf := revDerivUpdate K f x + (ydf.1 ^ n, + fun _ dy dx => ydf.2 (n * (conj ydf.1 ^ (n-1)) * dy) dx) := +by + unfold revDerivProjUpdate; + ftrans; simp[revDerivUpdate] + + +-- EnumType.sum ---------------------------------------------------------------- +-------------------------------------------------------------------------------- + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDerivProj_rule {ι : Type _} [EnumType ι] + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDerivProj K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun i dy => Id.run do + let mut dx : X := 0 + for j in fullRange ι do + dx := ydf.2 (j,i) dy dx + dx) := by sorry_proof + + +@[ftrans] +theorem SciLean.EnumType.sum.arg_f.revDerivProjUpdate_rule {ι : Type _} [EnumType ι] + (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) + : revDerivProjUpdate K (fun x => ∑ i, f x i) + = + fun x => + let ydf := revDerivProjUpdate K f x + (∑ i, ydf.1 i, + fun i dy dx => Id.run do + let mut dx : X := dx + for j in fullRange ι do + dx := ydf.2 (j,i) dy dx + dx) := +by + sorry_proof + + +-------------------------------------------------------------------------------- + +section InnerProductSpace + +variable + {R : Type _} [RealScalar R] + -- {K : Type _} [Scalar R K] + {X : Type _} [SemiInnerProductSpace R X] + {X Xi : Type _} {XI : Xi → Type _} [StructLike X Xi XI] [EnumType Xi] + {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi] + [SemiHilbert R Y] [∀ i, SemiHilbert R (YI i)] [SemiInnerProductSpaceStruct R Y Yi YI] + [SemiInnerProductSpace R X] [∀ i, SemiInnerProductSpace R (XI i)] [SemiInnerProductSpaceStruct R X Xi XI] + + -- [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI] + -- [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)] [SemiInnerProductSpaceStruct K Z Zi ZI] + -- {W : Type _} [SemiInnerProductSpace K W] + + +-- Inner ----------------------------------------------------------------------- +-------------------------------------------------------------------------------- + +open ComplexConjugate + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDerivProj_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDerivProj R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revCDeriv R f x + let y₂dg := revDerivUpdate R g x + let dx₁ := y₁df.2 y₂dg.1 + let dx₂ := y₂dg.2 y₁df.1 + (⟪y₁df.1, y₂dg.1⟫[R], + fun i dr => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (conj dr • y₂dg.1))) := +by + sorry_proof + +@[ftrans] +theorem Inner.inner.arg_a0a1.revDerivProjUpdate_rule + (f : X → Y) (g : X → Y) + (hf : HasAdjDiff R f) (hg : HasAdjDiff R g) + : (revDerivProjUpdate R fun x => ⟪f x, g x⟫[R]) + = + fun x => + let y₁df := revDerivUpdate R f x + let y₂dg := revDerivUpdate R g x + let dx₁ := y₁df.2 y₂dg.1 + let dx₂ := y₂dg.2 y₁df.1 + (⟪y₁df.1, y₂dg.1⟫[R], + fun i dr dx => + y₂dg.2 (dr • y₁df.1) (y₁df.2 (conj dr • y₂dg.1) dx) ) := +by + unfold revDerivProjUpdate + ftrans; simp[add_assoc,revDerivUpdate] + + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDerivProj_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDerivProj R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revCDeriv R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun _ dr => + ydf.2 (((2:R)*dr)•ydf.1)) := +by + sorry_proof + +@[ftrans] +theorem SciLean.Norm2.norm2.arg_a0.revDerivProjUpdate_rule + (f : X → Y) (hf : HasAdjDiff R f) + : (revDerivProjUpdate R fun x => ‖f x‖₂²[R]) + = + fun x => + let ydf := revDerivUpdate R f x + let ynorm2 := ‖ydf.1‖₂²[R] + (ynorm2, + fun _ dr dx => + ydf.2 (((2:R)*dr)•ydf.1) dx) := +by + unfold revDerivProjUpdate + ftrans; simp[revDerivUpdate, add_assoc] + + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDerivProj_rule_at + (f : X → Y) (x : X) + (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDerivProj R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revCDeriv R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun _ dr => + ydf.2 ((ynorm⁻¹ * dr)•ydf.1)):= +by + sorry_proof + + +@[ftrans] +theorem SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at + (f : X → Y) (x : X) + (hf : HasAdjDiffAt R f x) (hx : f x≠0) + : (revDerivProjUpdate R (fun x => ‖f x‖₂[R]) x) + = + let ydf := revDerivUpdate R f x + let ynorm := ‖ydf.1‖₂[R] + (ynorm, + fun _ dr dx => + ydf.2 ((ynorm⁻¹ * dr)•ydf.1) dx):= +by + unfold revDerivProjUpdate + ftrans; simp[revDerivUpdate, add_assoc] + +end InnerProductSpace + + + +#exit +section Test + +variable {K : Type _} [RealScalar K] + +set_option trace.Meta.Tactic.simp.discharge true in +#check + (revDerivProj K fun x : K×K => x.1 + x.2) + rewrite_by ftrans only; simp[StructLike.modify,StructLike.make] + + +set_option trace.Meta.Tactic.simp.discharge true in +#check + (revDerivProj K fun x : K×K => x.1*x.2 + x.2) + rewrite_by ftrans only; simp[StructLike.modify,StructLike.make] + + +set_option trace.Meta.Tactic.simp.rewrite true in +#check + (revDerivProj K fun x : K×K => x.1*x.2) + rewrite_by + ftrans only + simp only[StructLike.modify,StructLike.make,dite_eq_ite,eq_self,ite_true,dite_false] + +#exit + +set_option trace.Meta.Tactic.simp.rewrite true in +#check + (revDerivProj K fun x : K×K×K×K => x.1 + x.2.1 + x.2.2.1 + x.2.2.2) + rewrite_by + ftrans only + simp only[StructLike.modify,StructLike.make,dite_eq_ite,eq_self,ite_true,dite_false] + + +set_option trace.Meta.Tactic.simp.discharge true in +set_option trace.Meta.Tactic.fprop.discharge true in +#check + (revCDeriv K fun x : K×K×K×K => x.1^(2:ℕ) + x.2.1^2 + x.2.2.1^2 + x.2.2.2^2) + rewrite_by ftrans only; simp + + +set_option trace.Meta.Tactic.simp.discharge true in +set_option trace.Meta.Tactic.fprop.discharge true in +#check + (revCDeriv K fun x : K×K => x.2^2 + x.1^2) + rewrite_by ftrans only; simp + + + + + diff --git a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean index 7358cf72..44089e55 100644 --- a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean +++ b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean @@ -24,11 +24,23 @@ def revDerivUpdate -- : HasSemiAdjoint K (fun y => (revDerivUpdate K f x).2 y k 0) := by unfold revDerivUpdate; ftrans; fprop @[simp, ftrans_simp] -theorem revDerivProj_fst (f : X → Y) (x : X) +theorem revDerivUpdate_fst (f : X → Y) (x : X) : (revDerivUpdate K f x).1 = f x := by rfl +@[simp, ftrans_simp] +theorem revDerivUpdate_snd_zero (f : X → Y) (x dx : X) + : (revDerivUpdate K f x).2 0 dx = dx := +by + simp[revDerivUpdate] + +@[simp, ftrans_simp] +theorem revDerivUpdate_snd_zero' (f : X → Y) (x : X) (dy : Y) + : (revDerivUpdate K f x).2 dy 0 = (revCDeriv K f x).2 dy := +by + simp[revDerivUpdate] + namespace revDerivUpdate diff --git a/SciLean/Data/StructLike/Algebra.lean b/SciLean/Data/StructLike/Algebra.lean index 0a8c1419..65ddddd1 100644 --- a/SciLean/Data/StructLike/Algebra.lean +++ b/SciLean/Data/StructLike/Algebra.lean @@ -30,6 +30,17 @@ class SemiInnerProductSpaceStruct (K X I XI) [StructLike X I XI] [IsROrC K] [Enu inner_proj : ∀ (x x' : X), ⟪x,x'⟫[K] = ∑ (i : I), ⟪proj x i, proj x' i⟫[K] testFun_proj : ∀ (x : X), TestFunction x ↔ (∀ i, TestFunction (proj x i)) +instance (priority:=low) {X} [Vec K X] : VecStruct K X Unit (fun _ => X) where + proj_add := by simp[StructLike.proj] + proj_smul := by simp[StructLike.proj] + proj_zero := by simp[StructLike.proj] + proj_continuous := sorry_proof + make_continuous := sorry_proof + +instance (priority:=low) {X} [SemiInnerProductSpace K X] : SemiInnerProductSpaceStruct K X Unit (fun _ => X) where + inner_proj := sorry_proof + testFun_proj := sorry_proof + @[reducible] instance [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] (i : I ⊕ J) : Vec K (Prod.TypeFun EI FJ i) := @@ -37,7 +48,6 @@ instance [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] (i : I ⊕ J) : Vec K (Prod | .inl _ => by infer_instance | .inr _ => by infer_instance - instance [Vec K E] [Vec K F] [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] [VecStruct K E I EI] [VecStruct K F J FJ] : VecStruct K (E×F) (I⊕J) (Prod.TypeFun EI FJ) where diff --git a/SciLean/Data/StructLike/Basic.lean b/SciLean/Data/StructLike/Basic.lean index 3ea3e92c..707b2a29 100644 --- a/SciLean/Data/StructLike/Basic.lean +++ b/SciLean/Data/StructLike/Basic.lean @@ -38,7 +38,7 @@ by /-- Every type is `StructLike` with `Unit` as index set. -/ -instance (priority:=low) : StructLike α Unit (fun _ => α) where +instance (priority:=low) instStructLikeDefault : StructLike α Unit (fun _ => α) where proj := fun x _ => x make := fun f => f () modify := fun _ f x => f x