Documentation

Papers.OrendayLaresRockel2026TauFootruleBeta.JointVolume

← Mathematical handbook

Section 5: section areas, their unique maximum, and volume #

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.lowerFootrule (b : ℝ) :

Equations

Papers.OrendayLaresRockel2026TauFootruleBeta.lowerFootrule b = 3 / 16 * (1 + b) ^ 2 - 1 / 2

Instances For

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.upperFootrule (b : ℝ) :

Equations

Papers.OrendayLaresRockel2026TauFootruleBeta.upperFootrule b = 1 - 3 / 8 * (1 - b) ^ 2

Instances For

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea (b : ℝ) :

Equations

Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea b = 3 / 256 * (3 - b) ^ 2 * (1 + b) * (5 - 3 * b)

Instances For

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footrule_limits (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :

lowerFootrule b ≤ upperFootrule b ∧ upperFootrule b ≤ 1

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_nonneg (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :

0 ≤ sectionArea b

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_integral (b : ℝ) :

∫ (p : ℝ) in lowerFootrule b..upperFootrule b, 2 / 3 * (1 - p) = sectionArea b

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.fixed_beta_section_area (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :

MeasureTheory.volume {z : ℝ × ℝ | (z.1, z.2, b) ∈ jointRegion } = ENNReal.ofReal (sectionArea b)

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_integral_total :

∫ (b : ℝ) in -1..1, sectionArea b = 31 / 40

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_derivative (b : ℝ) :

HasDerivAt sectionArea (3 / 64 * (3 - b) * (3 * (b - 1) ^ 2 - 4)) b

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_maximum (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :

sectionArea b ≤ 1 / 4 + √3 / 6 ∧ (sectionArea b = 1 / 4 + √3 / 6 ↔ b = 1 - 2 / √3)

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion_volume :

MeasureTheory.volume jointRegion = ENNReal.ofReal (31 / 40)

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.sectionArea_maximum_attained :

1 - 2 / √3 ∈ Set.Icc (-1) 1 ∧ sectionArea (1 - 2 / √3) = 1 / 4 + √3 / 6