theorem NN.MLTheory.Proofs.UniversalApproximation.relu_universal_approximation_Icc
  {f : ℝ → ℝ} {a b L : ℝ} (h_ab : a < b)
  (hL : 0 < L)
  (h_lip :
    ∀ x ∈ Set.Icc a b,
      ∀ y ∈ Set.Icc a b,
        |f x - f y| ≤ L * |x - y|)
  (ε : ℝ) :
  ε > 0 →
    ∃ hidDim l1 l2,
      ∀ x ∈ Set.Icc a b,
        |f x -
              NN.MLTheory.Proofs.UniversalApproximation.mlpEval1d
                hidDim l1 l2 x| <
          ε

theorem NN.Proofs.Probability.isGaussian_forwardKernel.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  (a b : ℝ) (x : E) :
  ProbabilityTheory.IsGaussian
    ((NN.Proofs.Probability.forwardKernel
        a b)
      x)

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_progress
  {n : ℕ} (p : Spec.Hopfield.Params ℝ n)
  (hsym :
    NN.MLTheory.Proofs.Hopfield.SymmetricW
      p)
  (hdiag :
    NN.MLTheory.Proofs.Hopfield.DiagonalZero
      p)
  (s : Spec.Hopfield.State n)
  (hchange :
    NN.MLTheory.Proofs.Hopfield.cycleUpdate
        p s ≠
      s) :
  Spec.Hopfield.energy p
        (NN.MLTheory.Proofs.Hopfield.cycleUpdate
          p s) <
      Spec.Hopfield.energy p s ∨
    Spec.Hopfield.energy p
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate
            p s) =
        Spec.Hopfield.energy p s ∧
      Spec.Hopfield.pluses
          (NN.MLTheory.Proofs.Hopfield.cycleUpdate
            p s) >
        Spec.Hopfield.pluses s

theorem NN.MLTheory.Proofs.Hopfield.cycleUpdate_no_nontrivial_cycles
  {n : ℕ} (p : Spec.Hopfield.Params ℝ n)
  (hsym :
    NN.MLTheory.Proofs.Hopfield.SymmetricW
      p)
  (hdiag :
    NN.MLTheory.Proofs.Hopfield.DiagonalZero
      p)
  {k : ℕ} (hk : 0 < k)
  (s : Spec.Hopfield.State n)
  (hcyc :
    (NN.MLTheory.Proofs.Hopfield.f p)^[k]
        s =
      s) :
  NN.MLTheory.Proofs.Hopfield.f p s = s

theorem Proofs.RL.Markov.bellmanOptimality_contraction
  {S A : Type} [MeasurableSpace S]
  [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A)
  (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A]
  (values₁ values₂ :
    Spec.RL.Markov.ValueFunction S)
  (hMeas₁ : Measurable values₁)
  (hMeas₂ : Measurable values₂)
  (hBdd₁ :
    BddAbove
      (Set.range fun s => |values₁ s|))
  (hBdd₂ :
    BddAbove
      (Set.range fun s => |values₂ s|)) :
  Proofs.RL.Markov.valueSupDist
      (Spec.RL.Markov.bellmanOptimality
        mdp values₁)
      (Spec.RL.Markov.bellmanOptimality
        mdp values₂) ≤
    mdp.discount *
      Proofs.RL.Markov.valueSupDist
        values₁ values₂

theorem Proofs.RL.Markov.bellmanOptimality_fixedPoint_unique
  {S A : Type} [MeasurableSpace S]
  [MeasurableSpace A] [Nonempty S]
  (mdp : Spec.RL.Markov.MDP S A)
  (valid : Spec.RL.Markov.Valid mdp)
  [Fintype A] [Nonempty A]
  (v w : Spec.RL.Markov.ValueFunction S)
  (hv :
    Spec.RL.Markov.bellmanOptimality mdp
        v =
      v)
  (hw :
    Spec.RL.Markov.bellmanOptimality mdp
        w =
      w)
  (hMeasV : Measurable v)
  (hMeasW : Measurable w)
  (hBddV :
    BddAbove (Set.range fun s => |v s|))
  (hBddW :
    BddAbove (Set.range fun s => |w s|)) :
  v = w

theorem NN.Proofs.Models.Attention.causalMask_blocks_future
  {n : ℕ} (i j : Fin n) (hij : ↑i < ↑j) :
  Spec.get2 (Spec.causalMask n) i j =
    false

theorem NN.Proofs.Models.Attention.hardMaskedSoftmaxSpec_causal_future_zero
  {n : ℕ}
  (scores :
    Spec.Tensor ℝ
      (Spec.Shape.dim n
        (Spec.Shape.dim n
          Spec.Shape.scalar)))
  (i j : Fin n) (hij : ↑i < ↑j) :
  Spec.get2
      (Spec.hardMaskedSoftmaxSpec scores
        (Spec.causalMask n))
      i j =
    0

theorem NN.MLTheory.StateSpace.compactMamba_runList_append_outputs_prefix
  {α : Type} [Context α]
  {inputDim stateDim outputDim : ℕ}
  (m :
    Models.MambaBlockSpec α inputDim
      stateDim outputDim)
  (h0 :
    Spec.Tensor α
      (Spec.Shape.dim stateDim
        Spec.Shape.scalar))
  (xs ys :
    List
      (Spec.Tensor α
        (Spec.Shape.dim inputDim
          Spec.Shape.scalar))) :
  List.take xs.length
      (m.runList h0 (xs ++ ys)).2 =
    (m.runList h0 xs).2

theorem NN.MLTheory.SelfSupervised.varianceTerm_collapsed_positive
  {gamma d : ℕ} (hγ : 0 < gamma) :
  0 <
    NN.MLTheory.SelfSupervised.varianceTerm
      gamma (List.replicate (d + 1) 0)