← Mathematical handbook

structure Verification.ExclusionBand : Type

A measurable horizontal hole of fixed width. Degenerate parameter limits are allowed.

• width : ℝ
• width_nonneg : 0 ≤ self.width
• width_lt_one : self.width < 1
• lower : ↑unitInterval → ℝ
• lower_measurable : Measurable self.lower
• lower_nonneg (u : ↑unitInterval) : 0 ≤ self.lower u
• lower_le (u : ↑unitInterval) : self.lower u ≤ 1 - self.width

noncomputable def Verification.ExclusionBand.density (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

• B.density p = if B.lower p.1 ≤ ↑p.2 ∧ ↑p.2 ≤ B.lower p.1 + B.width then 0 else 1 / (1 - B.width)

theorem Verification.ExclusionBand.density_measurable (B : ExclusionBand) : Measurable B.density

theorem Verification.ExclusionBand.density_mem (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : B.density p ∈ Set.Icc 0 (1 / (1 - B.width))

theorem Verification.ExclusionBand.density_integrable (B : ExclusionBand) : MeasureTheory.Integrable B.density MeasureTheory.volume

theorem Verification.ExclusionBand.density_row_integrable (B : ExclusionBand) (u : ↑unitInterval) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => B.density (u, v)) MeasureTheory.volume

theorem Verification.ExclusionBand.density_row_integral (B : ExclusionBand) (u : ↑unitInterval) : ∫ (v : ↑unitInterval), B.density (u, v) = 1

theorem Verification.ExclusionBand.density_integral (B : ExclusionBand) : ∫ (p : ↑unitInterval × ↑unitInterval), B.density p = 1

noncomputable def Verification.ExclusionBand.measure (B : ExclusionBand) : MeasureTheory.Measure (↑unitInterval × ↑unitInterval)

Equations

• B.measure = MeasureTheory.volume.withDensity fun (p : ↑unitInterval × ↑unitInterval) => ENNReal.ofReal (B.density p)

instance Verification.ExclusionBand.instIsProbabilityMeasureProdElemRealUnitIntervalMeasure (B : ExclusionBand) : MeasureTheory.IsProbabilityMeasure B.measure

theorem Verification.ExclusionBand.integral_measure (B : ExclusionBand) (f : ↑unitInterval × ↑unitInterval → ℝ) : ∫ (p : ↑unitInterval × ↑unitInterval), f p ∂B.measure = ∫ (p : ↑unitInterval × ↑unitInterval), B.density p * f p

theorem Verification.ExclusionBand.map_fst (B : ExclusionBand) : MeasureTheory.Measure.map Prod.fst B.measure = MeasureTheory.volume

noncomputable def Verification.ExclusionBand.secondLaw (B : ExclusionBand) : MeasureTheory.Measure ℝ

Equations

• B.secondLaw = MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => ↑p.2) B.measure

instance Verification.ExclusionBand.instIsProbabilityMeasureRealSecondLaw (B : ExclusionBand) : MeasureTheory.IsProbabilityMeasure B.secondLaw

instance Verification.ExclusionBand.instNullSingletonClassRealSecondLaw (B : ExclusionBand) : MeasureTheory.NullSingletonClass B.secondLaw

noncomputable def Verification.ExclusionBand.sample (B : ExclusionBand) (p : ↑unitInterval × ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• B.sample p = ![p.1, ProbabilityTheory.cdfUnit B.secondLaw ↑p.2]

theorem Verification.ExclusionBand.sample_measurable (B : ExclusionBand) : Measurable B.sample

theorem Verification.ExclusionBand.sample_marginal (B : ExclusionBand) (d : Fin 2) : MeasureTheory.Measure.map (fun (p : ↑unitInterval × ↑unitInterval) => B.sample p d) B.measure = MeasureTheory.volume

noncomputable def Verification.ExclusionBand.copula (B : ExclusionBand) : ProbabilityTheory.Copula 2

Standardize the second marginal of the uniform density outside the hole.

Equations

• B.copula = ProbabilityTheory.Copula.ofMap ⟨B.measure, ⋯⟩ B.sample ⋯ ⋯

theorem Verification.ExclusionBand.copula_law (B : ExclusionBand) : B.copula.toMeasure = MeasureTheory.Measure.map B.sample B.measure