Lax Lean Archive

Optimization problems

Lax213208.OptimizationProblem · concepts/Lax213208/OptimizationProblem.lean · lax-213208

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    An optimization problem specifies feasible solutions, nonnegative objective values, and whether to minimize or maximize. Instances and solutions are typed mathematical objects with fixed, injective representations. Input size is the binary size of the instance's structural arena.

    The predicates are relative to these representations. Input presentations should come from the archive's structural combinators or certified constructor derivations; injectivity alone does not exclude encoded advice.

    Concept map
    4 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Lean source view on GitHub

    1import Mathlib.Data.NNReal.Basic
    2import Mathlib.Data.Set.Basic
    3import Lax560851.WordArena
    4import Lax759944.BinaryWordEncoding
    5
    6/-!
    7---
    8title: Optimization problems
    9type: definition
    10---
    11An optimization problem specifies feasible solutions, nonnegative objective
    12values, and whether to minimize or maximize. Instances and solutions are
    13typed mathematical objects with fixed, injective representations.
    14Input size is the binary size of the instance's structural arena.
    15
    16The predicates are relative to these representations. Input presentations
    17should come from the archive's structural combinators or certified
    18constructor derivations; injectivity alone does not exclude encoded advice.
    19-/
    20
    21namespace Lax213208.OptimizationProblem
    22
    23open scoped NNReal
    24open Lax560851.StructuralPresentation Lax560851.WordArena
    25open Lax759944.BinaryWordEncoding
    26
    27inductive Direction
    28 | minimize
    29 | maximize
    30
    31structure Problem (Instance Solution : Type*) where
    32 direction : Direction
    33 feasible : Instance → Solution → Prop
    34 value : Instance → Solution → ℝ≥0
    35 input : Presentation Instance
    36 output : Solution → List ℕ
    37 input_faithful : input.Faithful
    38 output_injective : Function.Injective output
    39
    40variable {Instance Solution : Type*}
    41
    42def inputWords (problem : Problem Instance Solution) (x : Instance) : List ℕ :=
    43 (encode problem.input x).toInput
    44
    45def inputSize (problem : Problem Instance Solution) (x : Instance) : ℕ :=
    46 bitSize (inputWords problem x)
    47
    48end Lax213208.OptimizationProblem
    49
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…