TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Proofs.Models.Mlp

Closed MLP Model Facts #

Small rational MLP examples belong in the proof layer. The forward composition law is already proved generally by Examples.mlp_spec_forward_eq; the facts below state a deterministic backward calculation as coordinate-level Lean theorems.

source
@[reducible, inline]
abbrev NN.Proofs.Models.Mlp.exInDim :
ℕ
Instances For
    source
    @[reducible, inline]
    abbrev NN.Proofs.Models.Mlp.exHidDim :
    ℕ
    Instances For
      source
      @[reducible, inline]
      abbrev NN.Proofs.Models.Mlp.exOutDim :
      ℕ
      Instances For
        source
        def NN.Proofs.Models.Mlp.exampleHiddenWeight :
        Spec.Tensor ℚ (Spec.Shape.dim exHidDim (Spec.Shape.dim exInDim Spec.Shape.scalar))
        Instances For
          source
          def NN.Proofs.Models.Mlp.exampleHiddenBias :
          Spec.Tensor ℚ (Spec.Shape.dim exHidDim Spec.Shape.scalar)
          Instances For
            source
            def NN.Proofs.Models.Mlp.exampleOutputWeight :
            Spec.Tensor ℚ (Spec.Shape.dim exOutDim (Spec.Shape.dim exHidDim Spec.Shape.scalar))
            Instances For
              source
              def NN.Proofs.Models.Mlp.exampleOutputBias :
              Spec.Tensor ℚ (Spec.Shape.dim exOutDim Spec.Shape.scalar)
              Instances For
                source
                def NN.Proofs.Models.Mlp.exampleHiddenLayer :
                Spec.LinearSpec ℚ exInDim exHidDim
                Instances For
                  source
                  def NN.Proofs.Models.Mlp.exampleOutputLayer :
                  Spec.LinearSpec ℚ exHidDim exOutDim
                  Instances For
                    source
                    def NN.Proofs.Models.Mlp.exInput :
                    Spec.Tensor ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar)
                    Instances For
                      source
                      def NN.Proofs.Models.Mlp.exNet :
                      ModSpec.SpecChain ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar) (Spec.Shape.dim exOutDim Spec.Shape.scalar)
                      Instances For
                        source
                        def NN.Proofs.Models.Mlp.exOutput :
                        Spec.Tensor ℚ (Spec.Shape.dim exOutDim Spec.Shape.scalar)
                        Instances For
                          source
                          def NN.Proofs.Models.Mlp.exExpected :
                          Spec.Tensor ℚ (Spec.Shape.dim exOutDim Spec.Shape.scalar)
                          Instances For
                            source
                            def NN.Proofs.Models.Mlp.exDLdy :
                            Spec.Tensor ℚ (Spec.Shape.dim exOutDim Spec.Shape.scalar)
                            Instances For
                              source
                              def NN.Proofs.Models.Mlp.exGrad :
                              Spec.Tensor ℚ (Spec.Shape.dim exHidDim (Spec.Shape.dim exInDim Spec.Shape.scalar)) × Spec.Tensor ℚ (Spec.Shape.dim exHidDim Spec.Shape.scalar) × Spec.Tensor ℚ (Spec.Shape.dim exOutDim (Spec.Shape.dim exHidDim Spec.Shape.scalar)) × Spec.Tensor ℚ (Spec.Shape.dim exOutDim Spec.Shape.scalar) × Spec.Tensor ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar)
                              Instances For
                                source
                                def NN.Proofs.Models.Mlp.exDXOpspec :
                                Spec.Tensor ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar)
                                Instances For
                                  source
                                  def NN.Proofs.Models.Mlp.dXHand :
                                  Spec.Tensor ℚ (Spec.Shape.dim exInDim Spec.Shape.scalar)
                                  Instances For