ML.Binary

theorem convexOn_softplus : ConvexOn ℝ univ softplus := by have hdiff : Differentiable ℝ softplus := fun x => (hasDerivAt_softplus x).differentiableAt have hderiv : deriv softplus = sigmoid := funext fun x => (hasDerivAt_softplus x).deriv exact Monotone.convexOn_univ_of_deriv hdiff (by simpa [hderiv] using Real.sigmoid_monotone)

theorem convexOn_logisticScoreLoss (y : Bool) : ConvexOn ℝ univ (fun t : ℝ => logisticScoreLoss y t) := by let lin : ℝ →ₗ[ℝ] ℝ := { toFun := fun t => -bool01 y * t map_add' := by intro a b ring map_smul' := by intro c a simp [smul_eq_mul] ring } have hlin : ConvexOn ℝ univ (fun t : ℝ => -bool01 y * t) := by simpa [Function.comp_def, lin] using (convexOn_id convex_univ).comp_linearMap lin -- `ConvexOn.add` concludes about the point-free sum `f + g`; put the goal in -- that shape and close by `exact`. simp only [logisticScoreLoss, sub_eq_add_neg, ← neg_mul] exact convexOn_softplus.add hlin

@[fun_prop] theorem continuous_logisticEmpRisk (Z : ι → E × Bool) : Continuous (logisticEmpRisk Z) := by classical unfold logisticEmpRisk have hscore : ∀ y : Bool, Continuous (fun t : ℝ => logisticScoreLoss y t) := by intro y simp only [logisticScoreLoss] exact continuous_softplus.sub (continuous_const.mul continuous_id) have hterm : ∀ i : ι, Continuous (fun β : E => logisticScoreLoss (Z i).2 (inner ℝ β (Z i).1)) := by intro i have hinner : Continuous (fun β : E => inner ℝ β (Z i).1) := by simpa [Function.comp_def] using continuous_inner.comp (continuous_id.prodMk continuous_const) exact (hscore (Z i).2).comp hinner have hsum : Continuous (fun β : E => ∑ i, logisticScoreLoss (Z i).2 (inner ℝ β (Z i).1)) := by exact continuous_finset_sum univ fun i _ => hterm i exact continuous_const.mul hsum

theorem regLogistic_basic_inequality (φ : FeatureMap γ K) (Z : ℕ → Ω → γ × ℝ) {lam : ℝ} (hlam : 0 < lam) (βstar : K → ℝ) (n : ℕ) (ω : Ω) {βhat : K → ℝ} (hFOC : regLogisticGrad φ Z lam n ω βhat = 0) : 2 * lam * ‖βhat - βstar‖ ≤ ∑ k, |regLogisticGrad φ Z lam n ω βstar k| := by classical let δ : K → ℝ := βhat - βstar let lin : (K → ℝ) → ℕ → ℝ := fun β i => ∑ j, β j * φ.φ (Z i ω).1 j let S0 : ℝ := ∑ k, (regLogisticGrad φ Z lam n ω βhat k - regLogisticGrad φ Z lam n ω βstar k) * δ k let a : ℕ → ℝ := fun i => sigmoid (lin βhat i) - sigmoid (lin βstar i) let b : ℕ → K → ℝ := fun i k => φ.φ (Z i ω).1 k have hgrad_diff : ∀ k, regLogisticGrad φ Z lam n ω βhat k - regLogisticGrad φ Z lam n ω βstar k = (n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k + 2 * lam * δ k := by intro k have hsum : (∑ i ∈ range n, (sigmoid (lin βhat i) - (Z i ω).2) * b i k) - (∑ i ∈ range n, (sigmoid (lin βstar i) - (Z i ω).2) * b i k) = ∑ i ∈ range n, a i * b i k := by rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl ?_ intro i _ dsimp [a] ring dsimp [regLogisticGrad, lin, b] change (n : ℝ)⁻¹ * (∑ i ∈ range n, (sigmoid (lin βhat i) - (Z i ω).2) * b i k) + 2 * lam * βhat k - ((n : ℝ)⁻¹ * (∑ i ∈ range n, (sigmoid (lin βstar i) - (Z i ω).2) * b i k) + 2 * lam * βstar k) = (n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k + 2 * lam * δ k rw [← hsum] dsimp [δ] ring_nf have hinner : ∀ i, ∑ k, b i k * δ k = lin βhat i - lin βstar i := by intro i dsimp [b, δ, lin] rw [← Finset.sum_sub_distrib] refine Finset.sum_congr rfl ?_ intro k _ ring have hsum_emp : ∑ k, ((n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k) * δ k = (n : ℝ)⁻¹ * ∑ i ∈ range n, a i * (lin βhat i - lin βstar i) := by calc ∑ k, ((n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k) * δ k = (n : ℝ)⁻¹ * ∑ k, (∑ i ∈ range n, a i * b i k) * δ k := by rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring _ = (n : ℝ)⁻¹ * ∑ k, ∑ i ∈ range n, (a i * b i k) * δ k := by congr 1 refine Finset.sum_congr rfl ?_ intro k _ rw [Finset.sum_mul] _ = (n : ℝ)⁻¹ * ∑ i ∈ range n, ∑ k, (a i * b i k) * δ k := by congr 1 rw [Finset.sum_comm] _ = (n : ℝ)⁻¹ * ∑ i ∈ range n, a i * (lin βhat i - lin βstar i) := by congr 1 refine Finset.sum_congr rfl ?_ intro i _ rw [← hinner i, Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring have hS_eq : S0 = (n : ℝ)⁻¹ * ∑ i ∈ range n, (sigmoid (lin βhat i) - sigmoid (lin βstar i)) * (lin βhat i - lin βstar i) + 2 * lam * ∑ k, (δ k) ^ 2 := by calc S0 = ∑ k, (((n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k + 2 * lam * δ k) * δ k) := by dsimp [S0] refine Finset.sum_congr rfl ?_ intro k _ rw [hgrad_diff] _ = ∑ k, ((n : ℝ)⁻¹ * ∑ i ∈ range n, a i * b i k) * δ k + ∑ k, (2 * lam * δ k) * δ k := by rw [← Finset.sum_add_distrib] refine Finset.sum_congr rfl ?_ intro k _ ring _ = (n : ℝ)⁻¹ * ∑ i ∈ range n, a i * (lin βhat i - lin βstar i) + 2 * lam * ∑ k, (δ k) ^ 2 := by rw [hsum_emp] congr 1 rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro k _ ring _ = (n : ℝ)⁻¹ * ∑ i ∈ range n, (sigmoid (lin βhat i) - sigmoid (lin βstar i)) * (lin βhat i - lin βstar i) + 2 * lam * ∑ k, (δ k) ^ 2 := rfl have hlog_nonneg : 0 ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, (sigmoid (lin βhat i) - sigmoid (lin βstar i)) * (lin βhat i - lin βstar i) := by exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg n)) (Finset.sum_nonneg fun i _ => monotone_mul_sub_nonneg Real.sigmoid_monotone (lin βhat i) (lin βstar i)) have hS_lower : 2 * lam * ∑ k, (δ k) ^ 2 ≤ S0 := by nlinarith [hS_eq, hlog_nonneg] have hS_grad : S0 = - ∑ k, regLogisticGrad φ Z lam n ω βstar k * δ k := by dsimp [S0, δ] simp [congrFun hFOC] have hneg_le_abs : - ∑ k, regLogisticGrad φ Z lam n ω βstar k * δ k ≤ ∑ k, |regLogisticGrad φ Z lam n ω βstar k| * |δ k| := by rw [← Finset.sum_neg_distrib] refine Finset.sum_le_sum ?_ intro k _ calc -(regLogisticGrad φ Z lam n ω βstar k * δ k) ≤ |regLogisticGrad φ Z lam n ω βstar k * δ k| := neg_le_abs _ _ = |regLogisticGrad φ Z lam n ω βstar k| * |δ k| := by rw [abs_mul] have hdot_bound : ∑ k, |regLogisticGrad φ Z lam n ω βstar k| * |δ k| ≤ (∑ k, |regLogisticGrad φ Z lam n ω βstar k|) * ‖δ‖ := by rw [Finset.sum_mul] refine Finset.sum_le_sum ?_ intro k _ have hcoord := norm_le_pi_norm δ k have habs : |δ k| ≤ ‖δ‖ := by simpa [Real.norm_eq_abs] using hcoord exact mul_le_mul_of_nonneg_left habs (abs_nonneg _) have hS_upper : S0 ≤ (∑ k, |regLogisticGrad φ Z lam n ω βstar k|) * ‖δ‖ := by calc S0 = - ∑ k, regLogisticGrad φ Z lam n ω βstar k * δ k := hS_grad _ ≤ ∑ k, |regLogisticGrad φ Z lam n ω βstar k| * |δ k| := hneg_le_abs _ ≤ (∑ k, |regLogisticGrad φ Z lam n ω βstar k|) * ‖δ‖ := hdot_bound have hquad : 2 * lam * ‖δ‖ ^ 2 ≤ (∑ k, |regLogisticGrad φ Z lam n ω βstar k|) * ‖δ‖ := by have hnormsq := pi_norm_sq_le_sum_sq δ have hleft : 2 * lam * ‖δ‖ ^ 2 ≤ 2 * lam * ∑ k, (δ k) ^ 2 := by exact mul_le_mul_of_nonneg_left hnormsq (by nlinarith) exact hleft.trans (hS_lower.trans hS_upper) by_cases hzero : ‖δ‖ = 0 · rw [show ‖βhat - βstar‖ = ‖δ‖ by rfl, hzero, mul_zero] exact Finset.sum_nonneg fun k _ => abs_nonneg _ · have hnorm_pos : 0 < ‖δ‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hzero) have hfinal : 2 * lam * ‖δ‖ ≤ ∑ k, |regLogisticGrad φ Z lam n ω βstar k| := by calc 2 * lam * ‖δ‖ = (2 * lam * ‖δ‖ ^ 2) / ‖δ‖ := by field_simp [hnorm_pos.ne'] _ ≤ ((∑ k, |regLogisticGrad φ Z lam n ω βstar k|) * ‖δ‖) / ‖δ‖ := by exact div_le_div_of_nonneg_right hquad hnorm_pos.le _ = ∑ k, |regLogisticGrad φ Z lam n ω βstar k| := by field_simp [hnorm_pos.ne'] simpa [δ] using hfinal

theorem regLogisticGrad_coord_isBigOp (φ : FeatureMap γ K) (P : Measure (γ × ℝ)) [IsProbabilityMeasure P] (S : IIDSample Ω (γ × ℝ) μ P) [IsProbabilityMeasure μ] {lam : ℝ} (βstar : K → ℝ) (hpop : IsPopulationRegLogistic P φ lam βstar) (hφ : ∀ k, Measurable (fun x => φ.φ x k)) (hscore : ∀ k, MemLp (fun z => (sigmoid (∑ j, βstar j * φ.φ z.1 j) - z.2) * φ.φ z.1 k) 2 P) (k : K) : IsBigOp (fun n ω => regLogisticGrad φ S.Z lam n ω βstar k) (fun n => (sqrt (n : ℝ))⁻¹) μ := by classical let g : γ × ℝ → ℝ := fun z => (sigmoid (∑ j, βstar j * φ.φ z.1 j) - z.2) * φ.φ z.1 k have hφ_prod : ∀ k, Measurable (fun z : γ × ℝ => φ.φ z.1 k) := fun k => (hφ k).comp measurable_fst have hg_meas : Measurable g := by fun_prop have hcoord : (fun n ω => regLogisticGrad φ S.Z lam n ω βstar k) = (fun n ω => S.sampleMean g n ω - ∫ z, g z ∂P) := by funext n ω have hpopk : (∫ z, g z ∂P) + 2 * lam * βstar k = 0 := by simpa [g] using hpop k dsimp [regLogisticGrad, IIDSample.sampleMean, g] linarith let A : ℝ := ∫ z, (g z) ^ 2 ∂P have hA_nonneg : 0 ≤ A := by dsimp [A] exact integral_nonneg fun z => sq_nonneg _ rw [hcoord] by_cases hA_pos : 0 < A · have hk0 := S.sampleMean_sub_isBigOp hg_meas (by simpa [g] using hscore k) (by simpa [A] using hA_pos) have hrate_le : ∀ n : ℕ, sqrt (A / (n : ℝ)) ≤ (sqrt A + 1) * (sqrt (n : ℝ))⁻¹ := by intro n calc sqrt (A / (n : ℝ)) = sqrt A * (sqrt (n : ℝ))⁻¹ := by rw [Real.sqrt_div hA_nonneg, div_eq_mul_inv] _ ≤ (sqrt A + 1) * (sqrt (n : ℝ))⁻¹ := by exact mul_le_mul_of_nonneg_right (by linarith [Real.sqrt_nonneg A]) (inv_nonneg.mpr (Real.sqrt_nonneg (n : ℝ))) have hk1 : IsBigOp (fun n ω => S.sampleMean g n ω - ∫ z, g z ∂P) (fun n => (sqrt A + 1) * (sqrt (n : ℝ))⁻¹) μ := by exact mono_rate hrate_le hk0 exact scale_rate (rn := fun n => (sqrt (n : ℝ))⁻¹) (by linarith [Real.sqrt_nonneg A]) hk1 · have hA_zero : A = 0 := le_antisymm (le_of_not_gt hA_pos) hA_nonneg intro δ hδ refine ⟨1, one_pos, ?_⟩ filter_upwards [Filter.eventually_gt_atTop (0 : ℕ)] with n hn have hsq := S.sampleMean_sub_sq_lintegral_le hg_meas (by simpa [g] using hscore k) hn have hlintegral_zero : ∫⁻ ω, ofReal ((S.sampleMean g n ω - ∫ z, g z ∂P) ^ 2) ∂μ = 0 := by apply le_antisymm · simpa [A, hA_zero] using hsq · exact bot_le have hae_sq : (fun ω => ofReal ((S.sampleMean g n ω - ∫ z, g z ∂P) ^ 2)) =ᵐ[μ] 0 := (lintegral_eq_zero_iff' (by fun_prop)).mp hlintegral_zero have hae_zero : (fun ω => S.sampleMean g n ω - ∫ z, g z ∂P) =ᵐ[μ] 0 := by filter_upwards [hae_sq] with ω hω simp only [Pi.zero_apply] at hω have hsquare_zero : (S.sampleMean g n ω - ∫ z, g z ∂P) ^ 2 = 0 := le_antisymm (ENNReal.ofReal_eq_zero.mp hω) (sq_nonneg _) exact sq_eq_zero_iff.mp hsquare_zero have hrate_pos : 0 < (sqrt (n : ℝ))⁻¹ := inv_pos.mpr (Real.sqrt_pos.mpr (by exact_mod_cast hn)) have hevent_zero : μ {ω | (1 : ℝ) * (sqrt (n : ℝ))⁻¹ ≤ ‖S.sampleMean g n ω - ∫ z, g z ∂P‖} = 0 := by rw [measure_eq_zero_iff_ae_notMem] filter_upwards [hae_zero] with ω hω simp [hω, not_le.mpr hrate_pos] calc μ {ω | (1 : ℝ) * (sqrt (n : ℝ))⁻¹ ≤ ‖S.sampleMean g n ω - ∫ z, g z ∂P‖} = 0 := hevent_zero _ ≤ δ := bot_le

theorem regLogisticCoef_isBigOp (φ : FeatureMap γ K) (P : Measure (γ × ℝ)) [IsProbabilityMeasure P] (S : IIDSample Ω (γ × ℝ) μ P) [IsProbabilityMeasure μ] {lam : ℝ} (hlam : 0 < lam) (βstar : K → ℝ) (βhat : ℕ → Ω → K → ℝ) (hpop : IsPopulationRegLogistic P φ lam βstar) (hFOC : ∀ n ω, regLogisticGrad φ S.Z lam n ω (βhat n ω) = 0) (hφ : ∀ k, Measurable (fun x => φ.φ x k)) (hscore : ∀ k, MemLp (fun z => (sigmoid (∑ j, βstar j * φ.φ z.1 j) - z.2) * φ.φ z.1 k) 2 P) : IsBigOp (fun n ω => ‖βhat n ω - βstar‖) (fun n => (sqrt (n : ℝ))⁻¹) μ := by classical let rn : ℕ → ℝ := fun n => (sqrt (n : ℝ))⁻¹ have hgrad_abs : ∀ k, IsBigOp (fun n ω => |regLogisticGrad φ S.Z lam n ω βstar k|) rn μ := by intro k simpa only [IsBigOp, BoundedInProbability, Real.norm_eq_abs, abs_abs, rn] using (regLogisticGrad_coord_isBigOp φ P S βstar hpop hφ hscore k) have hrn_pos : ∀ᶠ n : ℕ in atTop, 0 < rn n := (Filter.eventually_gt_atTop (0 : ℕ)).mono fun n hn => inv_pos.mpr (Real.sqrt_pos.mpr (by exact_mod_cast hn)) have hsum_abs : IsBigOp (fun n ω => ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k|) rn μ := by simpa using (IsBigOp.finset_sum (μ := μ) (s := (Finset.univ : Finset K)) (X := fun k n ω => |regLogisticGrad φ S.Z lam n ω βstar k|) hrn_pos (fun k _ => hgrad_abs k)) have hscaled : IsBigOp (fun n ω => (1 / (2 * lam)) * ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k|) rn μ := by exact IsBigOp.const_mul (μ := μ) (c := 1 / (2 * lam)) hsum_abs refine IsBigOp.of_abs_le (Xn := fun n ω => ‖βhat n ω - βstar‖) (Yn := fun n ω => (1 / (2 * lam)) * ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k|) ?_ hscaled intro n ω have hden_pos : 0 < 2 * lam := by nlinarith have hbound0 := regLogistic_basic_inequality φ S.Z hlam βstar n ω (hFOC n ω) have hsum_nonneg : 0 ≤ ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k| := Finset.sum_nonneg fun k _ => abs_nonneg _ have hscale_nonneg : 0 ≤ (1 / (2 * lam)) * ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k| := by exact mul_nonneg (le_of_lt (one_div_pos.mpr hden_pos)) hsum_nonneg rw [abs_of_nonneg (norm_nonneg _), abs_of_nonneg hscale_nonneg] calc ‖βhat n ω - βstar‖ = (2 * lam)⁻¹ * ((2 * lam) * ‖βhat n ω - βstar‖) := by field_simp [hden_pos.ne'] _ ≤ (2 * lam)⁻¹ * ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k| := by exact mul_le_mul_of_nonneg_left hbound0 (inv_nonneg.mpr hden_pos.le) _ = (1 / (2 * lam)) * ∑ k, |regLogisticGrad φ S.Z lam n ω βstar k| := by ring