A Property Kind Calculus for Measurement Metrology

19.7. Coverage intervals (R18)🔗

Once an output's uncertainty is a distribution, VIM 2.36–2.38 ask for a coverage interval — a probability attached to an interval about the mean. R18 discharges this in two tiers, graded by how much is assumed about the distribution's shape. Both are stated over ℝ and depend only on the variance the descriptor already carries; neither needs a true value (the sense in which coverage is provable while accuracy — closeness to nature — is not). Deliberately out of scope: exact normal coverage (the 95% ↔ k \approx 1.96 statement), which needs the Gaussian CDF / error function Mathlib does not provide, and any bridge to the executable Float sampler (the R15 exec↔spec axis).

Definition19.7.1
Group: The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. (28)
Group member previews
Preview
Definition 19.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

The standard uncertainty u = \sqrt{\mathrm{variance}} (VIM 2.30) — the scale in which a coverage interval is measured. It is the square root of the \kappa_2 the moment descriptor records.

Lean code for Definition19.7.1●1 definition
  • defdefined in PropertyKindCalculus/Uncertainty/Coverage.lean
    complete
    def PropertyKindCalculus.Uncertainty.Coverage.stdUnc.{u_1} {Ω : Type u_1}
  [MeasurableSpace Ω] (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ
    def PropertyKindCalculus.Uncertainty.Coverage.stdUnc.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  (X : Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) : ℝ
    The **standard uncertainty** `u = √variance` (VIM 2.30).
Proof for Definition 19.7.1
uses 0

Realized: Coverage.stdUnc, Real.sqrt of ProbabilityTheory.variance.

Theorem19.7.2
Group: The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. (28)
Group member previews
Preview
Definition 19.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagscapstoneproved

Tier 1 — the distribution-free coverage bound. For any distribution with a positive variance, the interval of k standard uncertainties about the mean, [m - k u,\, m + k u], has coverage probability at least 1 - 1/k^2. This is the complement of Chebyshev's inequality and assumes nothing about the distribution's shape. It is honest but conservative: k = 2 gives \ge 75\%, not the Gaussian 95\% — the famous figure is a shape assumption, out of scope. Uses the standard uncertainty.

Lean code for Theorem19.7.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Uncertainty/Coverage.lean
    complete
    theorem PropertyKindCalculus.Uncertainty.Coverage.coverageBound_stdUnc.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ}
  (hXm : Measurable X) (hX : MeasureTheory.MemLp X 2 μ) {k : ℝ}
  (hk : 0 < k) (hv : 0 < ProbabilityTheory.variance X μ) :
  1 - ENNReal.ofReal (1 / k ^ 2) ≤
    μ
      {ω |
        |X ω - ∫ (x : Ω), X x ∂μ| <
          k * PropertyKindCalculus.Uncertainty.Coverage.stdUnc X μ}
    theorem PropertyKindCalculus.Uncertainty.Coverage.coverageBound_stdUnc.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → ℝ} (hXm : Measurable X)
  (hX : MeasureTheory.MemLp X 2 μ) {k : ℝ}
  (hk : 0 < k)
  (hv :
    0 < ProbabilityTheory.variance X μ) :
  1 - ENNReal.ofReal (1 / k ^ 2) ≤
    μ
      {ω |
        |X ω - ∫ (x : Ω), X x ∂μ| <
          k *
            PropertyKindCalculus.Uncertainty.Coverage.stdUnc
              X μ}
    **R18, Tier 1 (coverage-factor form).** The metrological headline: the interval of `k`
standard uncertainties about the mean has coverage probability `≥ 1 − 1/k²` (Chebyshev). Honest
and distribution-free; `k = 2 ⇒ ≥ 75%` (the Gaussian 95% is a *shape* assumption, out of scope).
Requires a genuine (positive) standard uncertainty.
Proof for Theorem 19.7.2
uses 0

Realized over ℝ: coverageBound_stdUnc, from Mathlib's meas_ge_le_variance_div_sq by taking the complement of the tail event (prob_compl_eq_one_sub) and substituting c = k u. Sorry-free ([propext, Classical.choice, Quot.sound]). The half-width form coverageBound (\ge 1 - \mathrm{variance}/c^2) is the underlying lemma.

Theorem19.7.3
Group: The uncertainty layer rests on one additive descriptor placed alongside a quantity's magnitude. It has two faces, matching its two consumers: carrier-parametric moment data (what the linearized methods consume and what the ℝ -level theorems are proved about), and a sampler (the inverse-CDF, the single primitive shared by the Monte Carlo and systematic methods). The support range is carried too, because it is exactly the datum the numerical-adequacy check needs — the architectural hinge that makes the two halves of this chapter one design. (28)
Group member previews
Preview
Definition 19.3.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

Tier 2 — exact coverage for a bounded family. For a uniform distribution on [m - δ, m + δ], the coverage of the centred interval [m - h, m + h] (with 0 \le h \le δ) is exactly h/δ — closed-form, from the distribution's definition, and tighter than the Chebyshev bound. A concrete witness (the identity on ℝ under volume conditioned to the support) shows the hypothesis is non-vacuous; the Coverage worked example checks the central half of a uniform on [-2, 2] has coverage exactly 1/2.

Lean code for Theorem19.7.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Uncertainty/Coverage.lean
    complete
    theorem PropertyKindCalculus.Uncertainty.Coverage.uniform_coverage_exact.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω}
  {X : Ω → ℝ} {m δ : ℝ} (hδ : 0 < δ)
  (hu :
    MeasureTheory.pdf.IsUniform X (Set.Icc (m - δ) (m + δ)) P
      MeasureTheory.volume)
  {h : ℝ} (_hh0 : 0 ≤ h) (hhδ : h ≤ δ) :
  P (X ⁻¹' Set.Icc (m - h) (m + h)) = ENNReal.ofReal (h / δ)
    theorem PropertyKindCalculus.Uncertainty.Coverage.uniform_coverage_exact.{u_1}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {P : MeasureTheory.Measure Ω}
  {X : Ω → ℝ} {m δ : ℝ} (hδ : 0 < δ)
  (hu :
    MeasureTheory.pdf.IsUniform X
      (Set.Icc (m - δ) (m + δ)) P
      MeasureTheory.volume)
  {h : ℝ} (_hh0 : 0 ≤ h) (hhδ : h ≤ δ) :
  P (X ⁻¹' Set.Icc (m - h) (m + h)) =
    ENNReal.ofReal (h / δ)
    **R18, Tier 2 (uniform, exact).** For `X` uniform on `[m − δ, m + δ]` (`δ > 0`), the coverage
of the centred interval `[m − h, m + h]` (`0 ≤ h ≤ δ`) is *exactly* `h/δ` — closed-form, from the
uniform's definition, and tighter than the Chebyshev bound.
Proof for Theorem 19.7.3
uses 0

Realized over ℝ: uniform_coverage_exact, from Mathlib's pdf.IsUniform.measure_preimage and Real.volume_Icc (the intersection with the support is the sub-interval, and the ratio of Lebesgue lengths is 2h/2δ = h/δ). Sorry-free ([propext, Classical.choice, Quot.sound]).