audit-session038c-axioms.txt

Raw #print axioms transcript

'NguyenRH1.lambda_pos_finite_height_verified' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.marginTilde_convex' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.marginTilde_eq_expanded' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.marginTilde_eq_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
def NguyenRH1.Bn : (ℝ → ℝ) → ℝ → ℝ :=
fun F n =>
  have T := √n + 1;
  4 * F T + 4 * T * (2 / 3 * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 +
        2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3) +
      IIMaj n +
    1
def NguyenRH1.Z2hat : ℝ → ℝ :=
fun t => 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7
'NguyenRH1.Bn_FAlt_80000_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.Bn_FAlt_100000_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.marginTilde_FAlt_80000_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'NguyenRH1.marginTilde_FAlt_80000_lt_100000' depends on axioms: [propext, Classical.choice, Quot.sound]