noncomputable def BooleanFourier.twoPointLogPathFn (p a b t : ℝ) : ℝ

noncomputable def BooleanFourier.twoPointLogPathFn_derivValue (p a b t : ℝ) : ℝ

theorem BooleanFourier.twoPointLogPathFn_eq_log {p a b : ℝ} (hp : 1 < p) (ha : 0 < a) (hb : 0 < b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : twoPointLogPathFn p a b t = Real.log (((((1 + t) / 2 * a + (1 - t) / 2 * b) ^ (1 + (p - 1) / t ^ 2) + ((1 - t) / 2 * a + (1 + t) / 2 * b) ^ (1 + (p - 1) / t ^ 2)) / 2) ^ (1 / (1 + (p - 1) / t ^ 2)))

noncomputable def BooleanFourier.twoPointLogSumGap (p a b t : ℝ) : ℝ

theorem BooleanFourier.twoPointLogPathFn_deriv_decomp {p a b t : ℝ} (hp : 1 < p) (ht_pos : 0 < t) : twoPointLogPathFn_derivValue p a b t = have r := 1 + (p - 1) / t ^ 2; have c := (1 + t) / 2 * a + (1 - t) / 2 * b; have d := (1 - t) / 2 * a + (1 + t) / 2 * b; have S := c ^ r + d ^ r; have r' := -2 * (p - 1) / t ^ 3; have c' := (a - b) / 2; have d' := (b - a) / 2; (c ^ (r - 1) * c' + d ^ (r - 1) * d') / S + r' / r * twoPointLogSumGap p a b t

theorem BooleanFourier.twoPointLogSumGap_nonneg {p a b : ℝ} (hp : 1 < p) (ha : 0 < a) (hb : 0 < b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 ≤ twoPointLogSumGap p a b t

theorem BooleanFourier.logPathFn_hasDerivWithinAt {p a b : ℝ} (hp : 1 < p) (ha : 0 < a) (hb : 0 < b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivWithinAt (twoPointLogPathFn p a b) (twoPointLogPathFn_derivValue p a b t) (Set.Ioo 0 1) t

theorem BooleanFourier.logPathFn_deriv_nonneg {p a b : ℝ} (hp : 1 < p) (ha : 0 < a) (hb : 0 < b) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : 0 ≤ twoPointLogPathFn_derivValue p a b t

theorem BooleanFourier.twoPointLogPathFn_monotoneOn {p a b : ℝ} (hp : 1 < p) (ha : 0 < a) (hb : 0 < b) : MonotoneOn (twoPointLogPathFn p a b) (Set.Ioo 0 1)