noncomputable def ProbabilityTheory.statInfoFun (β : ℝ) (γ : ℝ) (x : ℝ) : ℝ

The hockey-stick function, it is related to the statistical information divergence.

Equations

• ProbabilityTheory.statInfoFun β γ x = if γ ≤ β then max 0 (γ - β * x) else max 0 (β * x - γ)

theorem ProbabilityTheory.statInfoFun_nonneg (β : ℝ) (γ : ℝ) (x : ℝ) : 0 ≤ ProbabilityTheory.statInfoFun β γ x

@[simp]

theorem ProbabilityTheory.statInfoFun_of_one {γ : ℝ} {x : ℝ} : ProbabilityTheory.statInfoFun 1 γ x = if γ ≤ 1 then max 0 (γ - x) else max 0 (x - γ)

@[simp]

theorem ProbabilityTheory.statInfoFun_of_zero {γ : ℝ} {x : ℝ} : ProbabilityTheory.statInfoFun 0 γ x = 0

theorem ProbabilityTheory.const_mul_statInfoFun {β : ℝ} {γ : ℝ} {x : ℝ} {a : ℝ} (ha : 0 ≤ a) : a * ProbabilityTheory.statInfoFun β γ x = ProbabilityTheory.statInfoFun (a * β) (a * γ) x

theorem ProbabilityTheory.statInfoFun_neg_neg {β : ℝ} {γ : ℝ} (h : β ≠ γ) : ProbabilityTheory.statInfoFun (-β) (-γ) = ProbabilityTheory.statInfoFun β γ

theorem ProbabilityTheory.stronglyMeasurable_statInfoFun : MeasureTheory.StronglyMeasurable (Function.uncurry (Function.uncurry ProbabilityTheory.statInfoFun))

theorem ProbabilityTheory.measurable_statInfoFun2 {β : ℝ} {x : ℝ} : Measurable fun (γ : ℝ) => ProbabilityTheory.statInfoFun β γ x

theorem ProbabilityTheory.stronglyMeasurable_statInfoFun3 {β : ℝ} {γ : ℝ} : MeasureTheory.StronglyMeasurable (ProbabilityTheory.statInfoFun β γ)

theorem ProbabilityTheory.statInfoFun_of_le {β : ℝ} {γ : ℝ} {x : ℝ} (h : γ ≤ β) : ProbabilityTheory.statInfoFun β γ x = max 0 (γ - β * x)

theorem ProbabilityTheory.statInfoFun_of_gt {β : ℝ} {γ : ℝ} {x : ℝ} (h : γ > β) : ProbabilityTheory.statInfoFun β γ x = max 0 (β * x - γ)

theorem ProbabilityTheory.statInfoFun_of_pos_of_le_of_le {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 < β) (hγ : γ ≤ β) (hx : x ≤ γ / β) : ProbabilityTheory.statInfoFun β γ x = γ - β * x

theorem ProbabilityTheory.statInfoFun_of_pos_of_le_of_ge {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 < β) (hγ : γ ≤ β) (hx : x ≥ γ / β) : ProbabilityTheory.statInfoFun β γ x = 0

theorem ProbabilityTheory.statInfoFun_of_pos_of_gt_of_le {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 < β) (hγ : γ > β) (hx : x ≤ γ / β) : ProbabilityTheory.statInfoFun β γ x = 0

theorem ProbabilityTheory.statInfoFun_of_pos_of_gt_of_ge {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 < β) (hγ : γ > β) (hx : x ≥ γ / β) : ProbabilityTheory.statInfoFun β γ x = β * x - γ

theorem ProbabilityTheory.statInfoFun_of_neg_of_le_of_le {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β < 0) (hγ : γ ≤ β) (hx : x ≤ γ / β) : ProbabilityTheory.statInfoFun β γ x = 0

theorem ProbabilityTheory.statInfoFun_of_neg_of_le_of_ge {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β < 0) (hγ : γ ≤ β) (hx : x ≥ γ / β) : ProbabilityTheory.statInfoFun β γ x = γ - β * x

theorem ProbabilityTheory.statInfoFun_of_neg_of_gt_of_le {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β < 0) (hγ : γ > β) (hx : x ≤ γ / β) : ProbabilityTheory.statInfoFun β γ x = β * x - γ

theorem ProbabilityTheory.statInfoFun_of_neg_of_gt_of_ge {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β < 0) (hγ : γ > β) (hx : x ≥ γ / β) : ProbabilityTheory.statInfoFun β γ x = 0

theorem ProbabilityTheory.statInfoFun_of_one_of_le_one {γ : ℝ} {x : ℝ} (h : γ ≤ 1) : ProbabilityTheory.statInfoFun 1 γ x = max 0 (γ - x)

theorem ProbabilityTheory.statInfoFun_of_one_of_one_lt {γ : ℝ} {x : ℝ} (h : 1 < γ) : ProbabilityTheory.statInfoFun 1 γ x = max 0 (x - γ)

theorem ProbabilityTheory.statInfoFun_of_one_of_le_one_of_le {γ : ℝ} {x : ℝ} (h : γ ≤ 1) (hx : x ≤ γ) : ProbabilityTheory.statInfoFun 1 γ x = γ - x

theorem ProbabilityTheory.statInfoFun_of_one_of_le_one_of_ge {γ : ℝ} {x : ℝ} (h : γ ≤ 1) (hx : x ≥ γ) : ProbabilityTheory.statInfoFun 1 γ x = 0

theorem ProbabilityTheory.statInfoFun_of_one_of_one_lt_of_le {γ : ℝ} {x : ℝ} (h : 1 < γ) (hx : x ≤ γ) : ProbabilityTheory.statInfoFun 1 γ x = 0

theorem ProbabilityTheory.statInfoFun_of_one_of_one_lt_of_ge {γ : ℝ} {x : ℝ} (h : 1 < γ) (hx : x ≥ γ) : ProbabilityTheory.statInfoFun 1 γ x = x - γ

theorem ProbabilityTheory.convexOn_statInfoFun (β : ℝ) (γ : ℝ) : ConvexOn ℝ Set.univ fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x

theorem ProbabilityTheory.derivAtTop_statInfoFun_of_nonneg_of_le {β : ℝ} {γ : ℝ} (hβ : 0 ≤ β) (hγ : γ ≤ β) : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) = 0

theorem ProbabilityTheory.derivAtTop_statInfoFun_of_nonneg_of_gt {β : ℝ} {γ : ℝ} (hβ : 0 ≤ β) (hγ : γ > β) : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) = ↑β

theorem ProbabilityTheory.derivAtTop_statInfoFun_of_nonpos_of_le {β : ℝ} {γ : ℝ} (hβ : β ≤ 0) (hγ : γ ≤ β) : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) = -↑β

theorem ProbabilityTheory.derivAtTop_statInfoFun_of_nonpos_of_gt {β : ℝ} {γ : ℝ} (hβ : β ≤ 0) (hγ : γ > β) : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) = 0

theorem ProbabilityTheory.derivAtTop_statInfoFun_eq {β : ℝ} {γ : ℝ} : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) = ↑(if 0 ≤ β then if γ ≤ β then 0 else β else if γ ≤ β then -β else 0)

theorem ProbabilityTheory.derivAtTop_statInfoFun_ne_top (β : ℝ) (γ : ℝ) : (derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x) ≠ ⊤

theorem ProbabilityTheory.derivAtTop_statInfoFun_nonneg (β : ℝ) (γ : ℝ) : 0 ≤ derivAtTop fun (x : ℝ) => ProbabilityTheory.statInfoFun β γ x

theorem ProbabilityTheory.statInfoFun_of_nonneg_of_right_le_one {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 ≤ β) (hx : x ≤ 1) : ProbabilityTheory.statInfoFun β γ x = (Set.Ioc (β * x) β).indicator (fun (y : ℝ) => y - β * x) γ

theorem ProbabilityTheory.statInfoFun_of_nonneg_of_one_le_right {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 ≤ β) (hx : 1 ≤ x) : ProbabilityTheory.statInfoFun β γ x = (Set.Ioc β (β * x)).indicator (fun (y : ℝ) => β * x - y) γ

theorem ProbabilityTheory.statInfoFun_of_nonpos_of_right_le_one {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β ≤ 0) (hx : x ≤ 1) : ProbabilityTheory.statInfoFun β γ x = (Set.Ioc β (β * x)).indicator (fun (y : ℝ) => β * x - y) γ

theorem ProbabilityTheory.statInfoFun_of_nonpos_of_one_le_right {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β ≤ 0) (hx : 1 ≤ x) : ProbabilityTheory.statInfoFun β γ x = (Set.Ioc (β * x) β).indicator (fun (y : ℝ) => y - β * x) γ

theorem ProbabilityTheory.statInfoFun_of_one_of_one_le_right {γ : ℝ} {x : ℝ} (h : 1 ≤ x) : ProbabilityTheory.statInfoFun 1 γ x = (Set.Ioc 1 x).indicator (fun (y : ℝ) => x - y) γ

theorem ProbabilityTheory.statInfoFun_of_one_of_right_le_one {γ : ℝ} {x : ℝ} (h : x ≤ 1) : ProbabilityTheory.statInfoFun 1 γ x = (Set.Ioc x 1).indicator (fun (y : ℝ) => y - x) γ

theorem ProbabilityTheory.statInfoFun_le_of_nonneg_of_right_le_one {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 ≤ β) (hx : x ≤ 1) : ProbabilityTheory.statInfoFun β γ x ≤ (Set.Ioc (β * x) β).indicator (fun (x_1 : ℝ) => β - β * x) γ

theorem ProbabilityTheory.statInfoFun_le_of_nonneg_of_one_le_right {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : 0 ≤ β) (hx : 1 ≤ x) : ProbabilityTheory.statInfoFun β γ x ≤ (Set.Ioc β (β * x)).indicator (fun (x_1 : ℝ) => β * x - β) γ

theorem ProbabilityTheory.statInfoFun_le_of_nonpos_of_right_le_one {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β ≤ 0) (hx : x ≤ 1) : ProbabilityTheory.statInfoFun β γ x ≤ (Set.Ioc β (β * x)).indicator (fun (x_1 : ℝ) => β * x - β) γ

theorem ProbabilityTheory.statInfoFun_le_of_nonpos_of_one_le_right {β : ℝ} {γ : ℝ} {x : ℝ} (hβ : β ≤ 0) (hx : 1 ≤ x) : ProbabilityTheory.statInfoFun β γ x ≤ (Set.Ioc (β * x) β).indicator (fun (x_1 : ℝ) => β - β * x) γ

theorem ProbabilityTheory.lintegral_nnnorm_statInfoFun_le {μ : MeasureTheory.Measure ℝ} (β : ℝ) (x : ℝ) : ∫⁻ (γ : ℝ), ↑‖ProbabilityTheory.statInfoFun β γ x‖₊ ∂μ ≤ μ (Ι (β * x) β) * ENNReal.ofReal |β - β * x|

theorem ProbabilityTheory.integrable_statInfoFun {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] (β : ℝ) (x : ℝ) : MeasureTheory.Integrable (fun (γ : ℝ) => ProbabilityTheory.statInfoFun β γ x) μ