TorchLean API

Docs HomeGuideExamplesGraphs

NN.MLTheory.Proofs.Approximation.FloatInterval.ConstantTarget

Constant rounded targets over Interval32 #

Exact interval-image theorem for constant rounded targets over IEEE32Exec.

This file packages the finite-float base case for the concrete IEEE32Exec.Interval32 interval type: a constant rounded target has exact interval semantics given by the point interval [c,c] on every valid input box.

The companion file FloatInterval.Semantics develops the same idea for the abstract interval domain I used by the MLP interval evaluator. We keep this file separate because it is the direct Interval32 statement used at the low-level rounded-target boundary, while FloatInterval.Semantics is the reusable abstract-domain semantics.

source
@[reducible, inline]
abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.F :
Type

Shorthand for the float32 executable type IEEE32Exec.

Instances For
    source
    @[reducible, inline]
    abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.I :
    Type

    Shorthand for the float32 interval type IEEE32Exec.Interval32.

    Instances For
      source
      @[reducible, inline]
      abbrev NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.Box (d : ℕ) :
      Type

      Product box of float32 intervals.

      Instances For
        source
        def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.Icc (a b : F) :
        Set F

        Float interval set {x | a ≤ x ∧ x ≤ b} (avoids requiring Preorder).

        Instances For
          source
          def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.γI (J : I) :
          Set F

          Concretization of a float32 interval to a set of float32 values.

          Instances For
            source
            def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.γ {d : ℕ} (B : Box d) :
            Set (Fin d → F)

            Concretization of a product box to a set of float32 vectors.

            Instances For
              source
              def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.BoxValid {d : ℕ} (B : Box d) :
              Prop

              Basic “well-formedness” predicate for product boxes.

              Instances For
                source
                def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.BoxInCube {d : ℕ} (B : Box d) :
                Prop

                B is a box contained in [-1,1]^d.

                Instances For
                  source
                  def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.IsMinOn {X : Type} (g : X → F) (S : Set X) (m : F) :
                  Prop

                  m is a minimum of g on the set S, stated without choosing a canonical min.

                  Instances For
                    source
                    def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.IsMaxOn {X : Type} (g : X → F) (S : Set X) (M : F) :
                    Prop

                    M is a maximum of g on the set S, stated without choosing a canonical max.

                    Instances For
                      source
                      def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.ExactIntervalImage {d : ℕ} (g _ν : (Fin d → F) → F) (nuInt : Box d → I) :
                      Prop

                      Exact interval-image property, phrased as: for every valid input box B, the interval semantics nuInt(B)’s concretization is exactly the float interval between the min/max of the target’s direct image on γ(B).

                      We phrase extrema relationally, rather than through a chosen float min/max operator, because NaN-aware binary32 orders need their edge cases stated explicitly.

                      Instances For
                        source
                        def NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.RoundedTargetExactIntervalImageStatement (d : ℕ) :
                        Prop

                        Generic exact-interval-image statement shape for IEEE32Exec rounded targets.

                        Instances For
                          source
                          theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.le_refl_of_isFinite (x : F) (hx : TorchLean.Floats.IEEE754.IEEE32Exec.isFinite x = true) :
                          x ≤ x
                          source
                          theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.gamma_nonempty_of_BoxValid {d : ℕ} {B : Box d} (hB : BoxValid B) :
                          (γ B).Nonempty
                          source
                          theorem NN.MLTheory.Proofs.UniversalApproximation.FloatIntervalApprox.ConstantTarget.exactIntervalImage_constant {d : ℕ} (c : F) (hc : TorchLean.Floats.IEEE754.IEEE32Exec.isFinite c = true) :
                          ExactIntervalImage (fun (x : Fin d → F) => c) (fun (x : Fin d → F) => c) fun (x : Box d) => TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.point c

                          Base case: a constant target g(x) = c has an exact interval-image witness given by the constant network and the point interval [c,c].