ML.Binary

theorem bernoulliCE_isMinOn {η : ℝ} (hη : η ∈ Ioo (0 : ℝ) 1) : IsMinOn (fun q : ℝ => bernoulliCE η q) (Ioo (0 : ℝ) 1) η := by rw [isMinOn_iff] intro q hq rcases hη with ⟨hη0, hη1⟩ rcases hq with ⟨hq0, hq1⟩ have hη1pos : 0 < 1 - η := sub_pos.mpr hη1 have hq1pos : 0 < 1 - q := sub_pos.mpr hq1 have hlog1 : log q - log η ≤ q / η - 1 := by simpa [Real.log_div hq0.ne' hη0.ne'] using (Real.log_le_sub_one_of_pos (div_pos hq0 hη0)) have hineq1 : η * (log q - log η) ≤ q - η := by have hmul := mul_le_mul_of_nonneg_left hlog1 hη0.le have hrhs : η * (q / η - 1) = q - η := by field_simp [hη0.ne'] simpa [hrhs] using hmul have hlog2 : log (1 - q) - log (1 - η) ≤ (1 - q) / (1 - η) - 1 := by simpa [Real.log_div hq1pos.ne' hη1pos.ne'] using (Real.log_le_sub_one_of_pos (div_pos hq1pos hη1pos)) have hineq2 : (1 - η) * (log (1 - q) - log (1 - η)) ≤ η - q := by have hmul := mul_le_mul_of_nonneg_left hlog2 hη1pos.le have hrhs : (1 - η) * ((1 - q) / (1 - η) - 1) = η - q := by field_simp [hη1pos.ne'] ring simpa [hrhs] using hmul have hsum : η * log q + (1 - η) * log (1 - q) ≤ η * log η + (1 - η) * log (1 - η) := by nlinarith [hineq1, hineq2] unfold bernoulliCE nlinarith

theorem convexOn_logisticEmpRisk (Z : ι → E × Bool) : ConvexOn ℝ univ (logisticEmpRisk Z) := by classical unfold logisticEmpRisk have hsummand : ∀ i : ι, ConvexOn ℝ univ (fun β : E => logisticScoreLoss (Z i).2 (inner ℝ β (Z i).1)) := by intro i exact convexOn_comp_inner (convexOn_logisticScoreLoss (Z i).2) (Z i).1 have hfin : ∀ t : Finset ι, ConvexOn ℝ univ (fun β : E => t.sum fun i => logisticScoreLoss (Z i).2 (inner ℝ β (Z i).1)) := by intro t induction t using Finset.induction_on with | empty => simpa using (convexOn_const (𝕜 := ℝ) (E := E) (β := ℝ) (s := univ) (0 : ℝ) convex_univ) | insert i t hi ht => simp only [Finset.sum_insert hi] exact (hsummand i).add ht simpa [smul_eq_mul] using (hfin univ).smul (inv_nonneg.mpr (Nat.cast_nonneg (card ι)))

theorem regLogistic_achievesL2Rate (φ : 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)) (h4 : Integrable (fun z => (∑ k, (φ.φ z.1 k) ^ 2) ^ 2) P) (hscore : ∀ k, MemLp (fun z => (sigmoid (∑ j, βstar j * φ.φ z.1 j) - z.2) * φ.φ z.1 k) 2 P) : AchievesL2Rate (fun n ω => logisticPredictor φ (βhat n ω)) (logisticPredictor φ βstar) P (fun n => (sqrt (n : ℝ))⁻¹) μ := by classical rcases eLpNorm_predictor_sub_le φ P hφ h4 βstar with ⟨C, hC_nonneg, hC_bound⟩ have hcoef := regLogisticCoef_isBigOp φ P S hlam βstar βhat hpop hFOC hφ hscore let D : ℝ := (1 / 4 : ℝ) * C have hD_nonneg : 0 ≤ D := by dsimp [D] exact mul_nonneg (by norm_num) hC_nonneg have hpred_bound : ∀ n ω, (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal ≤ D * ‖βhat n ω - βstar‖ := by intro n ω let β : K → ℝ := βhat n ω let linDiff : γ → ℝ := fun x => (∑ k, β k * φ.φ x k) - ∑ k, βstar k * φ.φ x k have hlin_mem := linear_predictor_sub_memLp φ P hφ h4 β βstar have hlin_ne_top : eLpNorm linDiff 2 (P.map fst) ≠ ⊤ := by simpa [linDiff] using hlin_mem.eLpNorm_ne_top have hscale_ne_top : eLpNorm ((1 / 4 : ℝ) • linDiff) 2 (P.map fst) ≠ ⊤ := by rw [eLpNorm_const_smul] exact ENNReal.mul_ne_top (by simp) hlin_ne_top have hmono : eLpNorm (fun x => logisticPredictor φ β x - logisticPredictor φ βstar x) 2 (P.map fst) ≤ eLpNorm ((1 / 4 : ℝ) • linDiff) 2 (P.map fst) := by refine eLpNorm_mono (μ := P.map fst) (p := 2) (fun x => ?_) rw [Real.norm_eq_abs, Real.norm_eq_abs] dsimp [logisticPredictor, linDiff] have h := sigmoid_lipschitz_quarter.dist_le_mul (∑ k, β k * φ.φ x k) (∑ k, βstar k * φ.φ x k) simpa [Real.dist_eq, abs_sub_comm, div_eq_mul_inv] using h have hsig_le : (eLpNorm (fun x => logisticPredictor φ β x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal ≤ (1 / 4 : ℝ) * (eLpNorm linDiff 2 (P.map fst)).toReal := by calc (eLpNorm (fun x => logisticPredictor φ β x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal ≤ (eLpNorm ((1 / 4 : ℝ) • linDiff) 2 (P.map fst)).toReal := ENNReal.toReal_mono hscale_ne_top hmono _ = (1 / 4 : ℝ) * (eLpNorm linDiff 2 (P.map fst)).toReal := by rw [eLpNorm_const_smul] rw [ENNReal.toReal_mul] · norm_num [Real.norm_eq_abs] have hlin_bound : (eLpNorm linDiff 2 (P.map fst)).toReal ≤ C * ‖β - βstar‖ := by simpa [linDiff, β] using hC_bound β dsimp [D] nlinarith have hpred_finite : ∀ n ω, eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst) ≠ ⊤ := by intro n ω let β : K → ℝ := βhat n ω let linDiff : γ → ℝ := fun x => (∑ k, β k * φ.φ x k) - ∑ k, βstar k * φ.φ x k have hlin_mem := linear_predictor_sub_memLp φ P hφ h4 β βstar have hlin_ne_top : eLpNorm linDiff 2 (P.map fst) ≠ ⊤ := by simpa [linDiff] using hlin_mem.eLpNorm_ne_top have hscale_ne_top : eLpNorm ((1 / 4 : ℝ) • linDiff) 2 (P.map fst) ≠ ⊤ := by rw [eLpNorm_const_smul] exact ENNReal.mul_ne_top (by simp) hlin_ne_top have hmono : eLpNorm (fun x => logisticPredictor φ β x - logisticPredictor φ βstar x) 2 (P.map fst) ≤ eLpNorm ((1 / 4 : ℝ) • linDiff) 2 (P.map fst) := by refine eLpNorm_mono (μ := P.map fst) (p := 2) (fun x => ?_) rw [Real.norm_eq_abs, Real.norm_eq_abs] dsimp [logisticPredictor, linDiff] have h := sigmoid_lipschitz_quarter.dist_le_mul (∑ k, β k * φ.φ x k) (∑ k, βstar k * φ.φ x k) simpa [Real.dist_eq, abs_sub_comm, div_eq_mul_inv] using h exact ne_of_lt (lt_of_le_of_lt hmono (lt_top_iff_ne_top.mpr hscale_ne_top)) unfold AchievesL2Rate constructor · exact hpred_finite intro ε hε rcases hcoef ε hε with ⟨M0, hM0⟩ let M : ℝ := max M0 0 have hM0_le_M : M0 ≤ M := le_max_left M0 0 have hM_nonneg : 0 ≤ M := le_max_right M0 0 refine ⟨D * M, ?_⟩ have hlim_M : limsup (fun n : ℕ => μ {ω | M * (sqrt (n : ℝ))⁻¹ < |‖βhat n ω - βstar‖|}) atTop ≤ ofReal ε := by refine le_trans (Filter.limsup_le_limsup (Filter.Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω have hr_nonneg : 0 ≤ (sqrt (n : ℝ))⁻¹ := inv_nonneg.mpr (Real.sqrt_nonneg _) exact lt_of_le_of_lt (mul_le_mul_of_nonneg_right hM0_le_M hr_nonneg) hω refine le_trans (Filter.limsup_le_limsup (Filter.Eventually.of_forall ?_)) hlim_M intro n apply measure_mono intro ω hω by_cases hD_zero : D = 0 · have hpred_le_zero : (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal ≤ 0 := by simpa [hD_zero] using hpred_bound n ω have hpred_nonneg : 0 ≤ (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal := ENNReal.toReal_nonneg have hpred_abs : |(eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal| = 0 := by rw [abs_of_nonneg hpred_nonneg] exact le_antisymm hpred_le_zero hpred_nonneg rw [hD_zero, zero_mul, zero_mul] at hω have hpred_abs' : |(fun n ω => (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal) n ω| = 0 := by simpa using hpred_abs exfalso have hωlt : 0 < |(fun n ω => (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal) n ω| := by simpa using hω rw [hpred_abs'] at hωlt exact (lt_irrefl (0 : ℝ)) hωlt · have hD_pos : 0 < D := lt_of_le_of_ne hD_nonneg (Ne.symm hD_zero) have hpred_bound' : (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal ≤ D * ‖βhat n ω - βstar‖ := hpred_bound n ω have hpred_nonneg : 0 ≤ (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal := ENNReal.toReal_nonneg have hnorm_nonneg : 0 ≤ ‖βhat n ω - βstar‖ := norm_nonneg _ have hlt : D * (M * (sqrt (n : ℝ))⁻¹) < D * ‖βhat n ω - βstar‖ := by calc D * (M * (sqrt (n : ℝ))⁻¹) = (D * M) * (sqrt (n : ℝ))⁻¹ := by ring _ < |(eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal| := hω _ = (eLpNorm (fun x => logisticPredictor φ (βhat n ω) x - logisticPredictor φ βstar x) 2 (P.map fst)).toReal := by rw [abs_of_nonneg hpred_nonneg] _ ≤ D * ‖βhat n ω - βstar‖ := hpred_bound' have hlt' : M * (sqrt (n : ℝ))⁻¹ < ‖βhat n ω - βstar‖ := by nlinarith [hD_pos, hlt] simpa [abs_of_nonneg hnorm_nonneg] using hlt'