← Mathematical handbook

Flat-topped tents and their exact first two moments

noncomputable def Verification.flatTent (a v : ↑unitInterval) : ℝ

Equations

• Verification.flatTent a v = min (↑a) (Verification.medianWedge v)

noncomputable def Verification.flatTentDisplacement (a : ↑unitInterval) : StripDisplacement

Equations

• Verification.flatTentDisplacement a = { toFun := Verification.flatTent a, zero := ⋯, one := ⋯, lipschitz := ⋯ }

theorem Verification.flatTent_ramps (a v : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : flatTent a v = ↑a - ramp a v - ramp a (unitInterval.symm v)

theorem Verification.flatTent_ramps_disjoint (a v : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : ramp a v * ramp a (unitInterval.symm v) = 0

theorem Verification.integral_flatTent (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : ∫ (v : ↑unitInterval), flatTent a v = ↑a * (1 - ↑a)

theorem Verification.integral_flatTent_sq (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : ∫ (v : ↑unitInterval), flatTent a v ^ 2 = ↑a ^ 2 - 4 * ↑a ^ 3 / 3

theorem Verification.xi_flatTent (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : (twoStrip (flatTentDisplacement a)).chatterjeeXi = 2 * ↑a ^ 2 * (3 - 4 * ↑a)

theorem Verification.correlationRatio_flatTent (a : ↑unitInterval) (ha : ↑a ≤ 1 / 2) : correlationRatio (twoStrip (flatTentDisplacement a)) = 12 * ↑a ^ 2 * (1 - ↑a) ^ 2