← Mathematical handbook

structure Verification.IncreasingBand : Type

A measurable band of fixed positive width, with a uniform conditional law in each row.

• width : ℝ
• width_pos : 0 < self.width
• width_le_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.IncreasingBand.density (B : IncreasingBand) (p : ↑unitInterval × ↑unitInterval) : ℝ

Equations

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

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

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

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

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

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

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

Equations

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

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

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

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

Standardize the second marginal of the uniform density inside the band.

Equations

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

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