From d1f5051b32f8801214c76d4eb6cdedced94caf8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 28 Aug 2024 08:57:29 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat:=20`1=20-=20x=E2=81=BB=C2=B9=20?= =?UTF-8?q?=E2=89=A4=20log=20x`=20(#16209)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This inequality is surprisingly tricky to prove. `(2⁻¹ + x)⁻¹ ≤ log (1 + x⁻¹)` also holds but requires actual analysis to prove, and all I want is a numerical lower bound on `log (65 / 64)`. From LeanAPAP Co-authored-by: Bhavik Mehta --- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean index ffe83425fd545..ac860ad68c9a6 100644 --- a/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean @@ -275,6 +275,9 @@ theorem log_le_sub_one_of_pos {x : ℝ} (hx : 0 < x) : log x ≤ x - 1 := by convert add_one_le_exp (log x) rw [exp_log hx] +lemma one_sub_inv_le_log_of_pos (hx : 0 < x) : 1 - x⁻¹ ≤ log x := by + simpa [add_comm] using log_le_sub_one_of_pos (inv_pos.2 hx) + /-- Bound for `|log x * x|` in the interval `(0, 1]`. -/ theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x| < 1 := by have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1 From a6fe1c5cd81750610bc8f5f15fac261fa81c91c0 Mon Sep 17 00:00:00 2001 From: faenuccio Date: Wed, 28 Aug 2024 11:17:38 +0200 Subject: [PATCH 2/2] fixed valuationSubring instances --- Mathlib/RingTheory/Valuation/AlgebraInstances.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Valuation/AlgebraInstances.lean b/Mathlib/RingTheory/Valuation/AlgebraInstances.lean index 849f794bedd26..84fac7089372c 100644 --- a/Mathlib/RingTheory/Valuation/AlgebraInstances.lean +++ b/Mathlib/RingTheory/Valuation/AlgebraInstances.lean @@ -1,4 +1,3 @@ -#exit /- Copyright (c) 2024 María Inés de Frutos-Fernández, Filippo A. E. Nuccio. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -33,7 +32,7 @@ variable {K : Type*} [Field K] (v : Valuation K ℤₘ₀) (L : Type*) [Field L] namespace ValuationSubring -- Implementation note : this instance was automatic in Lean3 -instance smul : SMul v.valuationSubring (integralClosure v.valuationSubring L) := Algebra.toSMul +instance : Algebra v.valuationSubring L := Algebra.ofSubring v.valuationSubring.toSubring theorem algebraMap_injective : Injective (algebraMap v.valuationSubring L) := (NoZeroSMulDivisors.algebraMap_injective K L).comp (IsFractionRing.injective _ _) @@ -51,6 +50,8 @@ theorem isIntegral_of_mem_ringOfIntegers' {x : (integralClosure v.valuationSubri variable (E : Type _) [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] +-- Imprementation note: this instance was not needed until 28-08-2024 +instance : IsScalarTower v.valuationSubring L E := Subring.instIsScalarTowerSubtypeMem _ /-- Given an algebra between two field extensions `L` and `E` of a field `K` with a valuation `v`, create an algebra between their two rings of integers. -/ instance algebra :