Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

The Personnel example, with probabilities

Lax392996.ProbabilityExample · concepts/Lax392996/ProbabilityExample.lean · lax-392996

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

    Example

    The paper's Example 14: each tuple tit_i of the B[X]\mathcal{B}[X]-instance I^\hat I is kept with an independent probability, Pr⁡(t1)=0.5\Pr(t_1) = 0.5 and Pr⁡(t2)=0.7\Pr(t_2) = 0.7 (the others, unspecified in the paper, are 0.50.5 here), and the probability that Nairobi is in the answer of qcityq_{\mathrm{city}} is Pr⁡(t1∧t2)=0.5⋅0.7=0.35\Pr(t_1 \wedge t_2) = 0.5 \cdot 0.7 = 0.35. Variables are numbered from 0 here, from 1 in the paper.

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 6 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Data.Rat.Defs
    2import Mathlib.Tactic.NormNum
    3import Lax392996.BooleanFunctions
    4import Lax392996.Databases
    5import Lax392996.AnnotatedDatabases
    6import Lax392996.RelationalAlgebra
    7import Lax392996.ProbabilisticDatabases
    8import Lax392996.PersonnelExample
    9import Lax392996.ProvenanceExample
    10
    11/-!
    12---
    13title: The Personnel example, with probabilities
    14type: example
    15---
    16The paper's Example 14: each tuple tit_i of the B[X]\mathcal{B}[X]-instance
    17I^\hat I is kept with an independent probability, Pr⁡(t1)=0.5\Pr(t_1) = 0.5 and
    18Pr⁡(t2)=0.7\Pr(t_2) = 0.7 (the others, unspecified in the paper, are 0.50.5 here),
    19and the probability that Nairobi is in the answer of qcityq_{\mathrm{city}} is
    20Pr⁡(t1∧t2)=0.5⋅0.7=0.35\Pr(t_1 \wedge t_2) = 0.5 \cdot 0.7 = 0.35. Variables are numbered from 0
    21here, from 1 in the paper.
    22-/
    23
    24namespace Lax392996.ProbabilityExample
    25
    26open Lax392996.BooleanFunctions Lax392996.Databases Lax392996.AnnotatedDatabases
    27open Lax392996.RelationalAlgebra Lax392996.ProbabilisticDatabases
    28open Lax392996.PersonnelExample Lax392996.ProvenanceExample
    29
    30/-- The probabilities of the tuples: `0.5`, except `0.7` for the second one. -/
    31def P : ProbAssignment (Fin 7) where
    32 prob x := if x = 1 then 7/10 else 1/2
    33 prob_nonneg := by
    34 intro x
    35 split <;> norm_num
    36 prob_le_one := by
    37 intro x
    38 split <;> norm_num
    39
    40/-- Example 14: the probability that Nairobi is an answer is `0.35`. -/
    41axiom nairobi_probability :
    42 ProbAssignment.marginalProb P qcity instanceB !["Nairobi"] = 7/20
    43
    44end Lax392996.ProbabilityExample
    45
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…