Lax Lean Archive

Duplicating a matched prediction under all-pairs accumulation

Lax303562.Duplication · concepts/Lax303562/Duplication.lean · lax-303562

proven

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

    Theorem

    Some evaluators accumulate every (prediction, annotation) pair whose IoU clears the threshold, rather than a one-to-one matching. Under that rule a second copy of an already matched prediction, with IoU vv against the same annotation, adds vv to the numerator and one true positive to the denominator, and creates no false positive.

    The first statement says exactly when this raises the score: if and only if vv exceeds the current Panoptic Quality. The second says that under one-to-one matching the same copy cannot match (its annotation is taken), counts as a false positive, and strictly lowers the score whenever there is anything to lose. The third puts the two together: the same submission moves the metric in opposite directions depending on the counting rule.

    Hypotheses: 0<dennfpfn0 < den n fp fn says that there is at least one prediction or annotation, so the quotient is not the empty case.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1 dup_iff proven

    2 falsePositive_lt proven

    3 opposite_directions proven

    Lean source view on GitHub

    1import Lax303562.PanopticQuality
    2
    3/-!
    4---
    5title: Duplicating a matched prediction under all-pairs accumulation
    6type: theorem
    7---
    8Some evaluators accumulate *every* (prediction, annotation) pair whose IoU clears
    9the threshold, rather than a one-to-one matching. Under that rule a second copy
    10of an already matched prediction, with IoU `v` against the same annotation, adds
    11`v` to the numerator and one true positive to the denominator, and creates no
    12false positive.
    13
    14The first statement says exactly when this raises the score: if and only if `v`
    15exceeds the current Panoptic Quality. The second says that under one-to-one
    16matching the same copy cannot match (its annotation is taken), counts as a false
    17positive, and strictly lowers the score whenever there is anything to lose. The
    18third puts the two together: the same submission moves the metric in opposite
    19directions depending on the counting rule.
    20
    21Hypotheses: `0 < den n fp fn` says that there is at least one prediction or
    22annotation, so the quotient is not the empty case.
    23-/
    24
    25namespace Lax303562.Duplication
    26
    27open Lax303562.PanopticQuality
    28
    29/-- Under all-pairs accumulation, a duplicate with IoU `v` of an already matched
    30prediction raises the Panoptic Quality exactly when `v` is larger than the
    31current Panoptic Quality. -/
    32axiom dup_iff (s v : ℝ) (n fp fn : ℕ) (hd : 0 < den n fp fn) :
    33 pq s n fp fn < pq (s + v) (n + 1) fp fn ↔ pq s n fp fn < v
    34
    35/-- Under one-to-one matching the duplicate is a false positive, and any false
    36positive strictly lowers a positive score. -/
    37axiom falsePositive_lt (s : ℝ) (n fp fn : ℕ) (hs : 0 < s) (hd : 0 < den n fp fn) :
    38 pq s n (fp + 1) fn < pq s n fp fn
    39
    40/-- A duplicate better than the current score raises the metric under all-pairs
    41accumulation and lowers it under one-to-one matching. -/
    42axiom opposite_directions (s v : ℝ) (n fp fn : ℕ) (hs : 0 < s) (hd : 0 < den n fp fn)
    43 (hv : pq s n fp fn < v) :
    44 pq s n fp fn < pq (s + v) (n + 1) fp fn ∧ pq s n (fp + 1) fn < pq s n fp fn
    45
    46end Lax303562.Duplication
    47
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…