The proof
V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2 ?
Read explanation (PDF)Source
Main.lean · 64775 lines · 3.3 MB
Showing the first 500 of 64775 lines. The whole file is 3.3 MB; download it to read the rest.
end Bounty
/-!
Erdos 416(i): proof adapted to the restricted conjectures.io submission format.
Modified from Erdos416Submission (3).lean. Supporting proofs and dependency
license notices are retained. The server supplies the imports and outer namespace.
The separate verification harness checks the target type and permitted axioms.
-/
/- Consolidated component: Erdos416.lean. -/
section
/-
Foundational lemmas for the distinct-totient doubling law.
The unconditional real-variable limit is proved at the end of this file.
Only established lemmas are included below; there are no admitted analytic inputs.
-/
open Filter
open scoped Topology BigOperators Classical
namespace Erdos416Proof
/- Original line 41: Erdos416Proof.totientsUpTo -/
noncomputable def totientsUpTo (x : ℝ) : Finset ℕ :=
open scoped Classical in
(Finset.Icc 1 ⌊x⌋₊).filter (fun n => ∃ m : ℕ, m.totient = n)
/-- The exact distinct-totient counting function in Erdős 416(i). -/
/- Original line 46: Erdos416Proof.V -/
noncomputable def V (x : ℝ) : ℝ := (totientsUpTo x).card
/- Original line 48: Erdos416Proof.mem_totientsUpTo -/
theorem mem_totientsUpTo {x : ℝ} (hx : 0 ≤ x) {n : ℕ} :
n ∈ totientsUpTo x ↔
0 < n ∧ (n : ℝ) ≤ x ∧ ∃ m : ℕ, 0 < m ∧ m.totient = n := by
classical
simp only [totientsUpTo, Finset.mem_filter, Finset.mem_Icc]
constructor
· rintro ⟨⟨hn, hnx⟩, m, hm⟩
refine ⟨by omega, (Nat.le_floor_iff hx).mp hnx, m, ?_, hm⟩
exact Nat.totient_pos.mp (by omega)
· rintro ⟨hn, hnx, m, _, hm⟩
exact ⟨⟨by omega, (Nat.le_floor_iff hx).mpr hnx⟩, m, hm⟩
/- Original line 60: Erdos416Proof.totientsUpTo_mono -/
theorem totientsUpTo_mono : Monotone totientsUpTo := by
classical
intro x y hxy n hn
simp only [totientsUpTo, Finset.mem_filter, Finset.mem_Icc] at hn ⊢
exact ⟨⟨hn.1.1, hn.1.2.trans (Nat.floor_mono hxy)⟩, hn.2⟩
/- Original line 66: Erdos416Proof.V_nonneg -/
theorem V_nonneg (x : ℝ) : 0 ≤ V x := by
exact Nat.cast_nonneg _
/- Original line 69: Erdos416Proof.V_mono -/
theorem V_mono : Monotone V := by
intro x y hxy
unfold V
exact_mod_cast Finset.card_le_card (totientsUpTo_mono hxy)
/- Original line 74: Erdos416Proof.V_pos -/
theorem V_pos {x : ℝ} (hx : 1 ≤ x) : 0 < V x := by
have hm : 1 ∈ totientsUpTo x :=
(mem_totientsUpTo (by linarith)).mpr ⟨by norm_num, by simpa using hx,
1, by norm_num, Nat.totient_one⟩
unfold V
exact_mod_cast Finset.card_pos.mpr ⟨1, hm⟩
/- Original line 81: Erdos416Proof.eventually_V_pos -/
theorem eventually_V_pos : ∀ᶠ x : ℝ in atTop, 0 < V x :=
(eventually_ge_atTop 1).mono fun _ hx => V_pos hx
open scoped Classical in
/- Original line 85: Erdos416Proof.V_eq_standard_count -/
theorem V_eq_standard_count (x : ℝ) :
V x = ((Finset.Icc 1 ⌊x⌋₊).filter
(fun n => ∃ m : ℕ, m.totient = n)).card := by
classical
rfl
/- Largest prime factors, with the convention P⁺(1) = 1. -/
/- Original line 93: Erdos416Proof.largestPrimeFactor -/
def largestPrimeFactor (n : ℕ) : ℕ := max 1 (n.primeFactors.sup id)
/- Original line 95: Erdos416Proof.largestPrimeFactor_one -/
theorem largestPrimeFactor_one : largestPrimeFactor 1 = 1 := by
simp [largestPrimeFactor]
/- Original line 98: Erdos416Proof.one_le_largestPrimeFactor -/
theorem one_le_largestPrimeFactor (n : ℕ) : 1 ≤ largestPrimeFactor n :=
le_max_left _ _
/- Original line 101: Erdos416Proof.prime_le_largestPrimeFactor -/
theorem prime_le_largestPrimeFactor {n p : ℕ} (hn : 0 < n)
(hp : p.Prime) (hpn : p ∣ n) : p ≤ largestPrimeFactor n :=
(Finset.le_sup (f := id) (hp.mem_primeFactors hpn (Nat.ne_of_gt hn))).trans
(le_max_right _ _)
/- Original line 106: Erdos416Proof.largestPrimeFactor_prime -/
theorem largestPrimeFactor_prime {p : ℕ} (hp : p.Prime) :
largestPrimeFactor p = p := by
simp [Erdos416Proof.largestPrimeFactor_one, largestPrimeFactor, hp.primeFactors, hp.one_le]
/- Original line 110: Erdos416Proof.largestPrimeFactor_mul -/
theorem largestPrimeFactor_mul {m n : ℕ} (hm : 0 < m) (hn : 0 < n) :
largestPrimeFactor (m * n) = max (largestPrimeFactor m) (largestPrimeFactor n) := by
simp [Erdos416Proof.largestPrimeFactor_one, largestPrimeFactor, Nat.primeFactors_mul (Nat.ne_of_gt hm) (Nat.ne_of_gt hn),
Finset.sup_union, max_assoc, max_left_comm, max_comm]
/- Original line 115: Erdos416Proof.coprime_of_largestPrimeFactor_lt -/
theorem coprime_of_largestPrimeFactor_lt {n p : ℕ} (hn : 0 < n) (hp : p.Prime)
(h : largestPrimeFactor n < p) : p.Coprime n := by
rw [hp.coprime_iff_not_dvd]
intro hdvd
exact (not_le_of_gt h) (prime_le_largestPrimeFactor hn hp hdvd)
/- Original line 121: Erdos416Proof.mem_factored_range_iff -/
theorem mem_factored_range_iff {P n : ℕ} (hP : 1 ≤ P) :
n ∈ Nat.factoredNumbers (Finset.range (P + 1)) ↔
0 < n ∧ largestPrimeFactor n ≤ P := by
rw [Nat.mem_factoredNumbers_iff_primeFactors_subset]
constructor
· rintro ⟨hn, hs⟩
refine ⟨Nat.pos_of_ne_zero hn, max_le hP ?_⟩
apply Finset.sup_le
intro p hp
exact Nat.le_of_lt_succ (Finset.mem_range.mp (hs hp))
· rintro ⟨hn, hmax⟩
refine ⟨Nat.ne_of_gt hn, fun p hp => Finset.mem_range.mpr ?_⟩
apply Nat.lt_succ_of_le
exact (Finset.le_sup (f := id) hp).trans ((le_max_right _ _).trans hmax)
/- Original line 136: Erdos416Proof.totient_prod_primes -/
theorem totient_prod_primes (s : Finset ℕ) (hs : ∀ p ∈ s, p.Prime) :
(∏ p ∈ s, p).totient = ∏ p ∈ s, (p - 1) := by
revert hs
induction s using Finset.induction with
| empty => simp
| @insert p s hps ih =>
intro hs
have hp : p.Prime := hs p (Finset.mem_insert_self _ _)
have hs' : ∀ q ∈ s, q.Prime := fun q hq => hs q (Finset.mem_insert_of_mem hq)
have hcop : p.Coprime (∏ q ∈ s, q) := by
apply Nat.coprime_prod_right_iff.mpr
intro q hq
rw [hp.coprime_iff_not_dvd]
intro hdvd
have heq : p = q := (Nat.prime_dvd_prime_iff_eq hp (hs' q hq)).mp hdvd
exact hps (heq.symm ▸ hq)
rw [Finset.prod_insert hps, Nat.totient_mul hcop, Nat.totient_prime hp,
ih hs', Finset.prod_insert hps]
/- Original line 155: Erdos416Proof.totient_core -/
theorem totient_core (r : ℕ) (s : Finset ℕ) (hs : ∀ p ∈ s, p.Prime)
(hcop : ∀ p ∈ s, p.Coprime r) :
(r * ∏ p ∈ s, p).totient = r.totient * ∏ p ∈ s, (p - 1) := by
rw [Nat.totient_mul (Nat.coprime_prod_left_iff.mpr hcop).symm,
totient_prod_primes s hs]
/- Original line 161: Erdos416Proof.top_prime_extension -/
theorem top_prime_extension {a p : ℕ} (ha : 0 < a) (hp : p.Prime)
(htop : largestPrimeFactor a < p) :
(p * a).totient = (p - 1) * a.totient ∧ largestPrimeFactor (p * a) = p := by
constructor
· rw [Nat.totient_mul (coprime_of_largestPrimeFactor_lt ha hp htop),
Nat.totient_prime hp]
· rw [largestPrimeFactor_mul hp.pos ha, largestPrimeFactor_prime hp,
max_eq_left htop.le]
/- The finite-prime reciprocal-tail lemma (Lemma 5 of the manuscript). -/
/- Original line 172: Erdos416Proof.invTotient -/
noncomputable def invTotient (n : ℕ) : ℝ := (n.totient : ℝ)⁻¹
/- Original line 174: Erdos416Proof.invTotient_one -/
theorem invTotient_one : invTotient 1 = 1 := by
simp [invTotient]
/- Original line 177: Erdos416Proof.invTotient_nonneg -/
theorem invTotient_nonneg (n : ℕ) : 0 ≤ invTotient n := by
unfold invTotient
positivity
/- Original line 181: Erdos416Proof.invTotient_mul -/
theorem invTotient_mul {m n : ℕ} (h : m.Coprime n) :
invTotient (m * n) = invTotient m * invTotient n := by
simp [Erdos416Proof.invTotient_one, invTotient, Nat.totient_mul h, mul_comm]
/- Original line 185: Erdos416Proof.invTotient_prime_pow_succ -/
theorem invTotient_prime_pow_succ {p : ℕ} (hp : p.Prime) (e : ℕ) :
invTotient (p ^ (e + 1)) = ((p : ℝ) - 1)⁻¹ * ((p : ℝ)⁻¹) ^ e := by
simp [Erdos416Proof.invTotient_one, invTotient, Nat.totient_prime_pow_succ hp, Nat.cast_sub hp.one_le,
mul_comm]
/- Original line 190: Erdos416Proof.hasSum_invTotient_prime_pow -/
theorem hasSum_invTotient_prime_pow {p : ℕ} (hp : p.Prime) :
HasSum (fun e : ℕ => invTotient (p ^ e))
(1 + (p : ℝ) / ((p : ℝ) - 1) ^ 2) := by
have hp1 : 1 < (p : ℝ) := by exact_mod_cast hp.one_lt
have hp0 : 0 < (p : ℝ) := by linarith
have hpinv : (p : ℝ)⁻¹ < 1 := by
exact (inv_lt_one₀ hp0).mpr hp1
have hgeo := (hasSum_geometric_of_lt_one (inv_nonneg.mpr hp0.le) hpinv).mul_left
(((p : ℝ) - 1)⁻¹)
have halgebra : ((p : ℝ) - 1)⁻¹ * (1 - (p : ℝ)⁻¹)⁻¹ =
(p : ℝ) / ((p : ℝ) - 1) ^ 2 := by
have hpne : (p : ℝ) ≠ 0 := ne_of_gt hp0
have hpne1 : (p : ℝ) - 1 ≠ 0 := by linarith
field_simp
rw [halgebra] at hgeo
have htail : HasSum (fun e : ℕ => invTotient (p ^ (e + 1)))
((p : ℝ) / ((p : ℝ) - 1) ^ 2) := by
simpa only [invTotient_prime_pow_succ hp] using hgeo
simpa only [Finset.sum_range_one, pow_zero, invTotient_one, add_comm] using
(hasSum_nat_add_iff (f := fun e : ℕ => invTotient (p ^ e)) 1).mp htail
/- Original line 211: Erdos416Proof.summable_invTotient_factored -/
theorem summable_invTotient_factored (s : Finset ℕ) :
Summable (fun n : Nat.factoredNumbers s => invTotient n) := by
have h := EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
invTotient_one (@invTotient_mul)
(fun hp => (hasSum_invTotient_prime_pow hp).summable.norm) s
exact h.1.of_norm
/- Original line 218: Erdos416Proof.tsum_invTotient_factored -/
theorem tsum_invTotient_factored (s : Finset ℕ) :
(∑' n : Nat.factoredNumbers s, invTotient n) =
∏ p ∈ s with p.Prime, (1 + (p : ℝ) / ((p : ℝ) - 1) ^ 2) := by
have h := EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum
invTotient_one (@invTotient_mul)
(fun hp => (hasSum_invTotient_prime_pow hp).summable.norm) s
rw [h.2.tsum_eq]
apply Finset.prod_congr rfl
intro p hp
exact (hasSum_invTotient_prime_pow (Finset.mem_filter.mp hp).2).tsum_eq
/- Original line 229: Erdos416Proof.invTotient_factored_tail -/
theorem invTotient_factored_tail (s : Finset ℕ) {ε : ℝ} (hε : 0 < ε) :
∃ R : ℕ, ∀ t : Finset ℕ,
(∀ n ∈ t, n ∈ Nat.factoredNumbers s) →
(∀ n ∈ t, R < n) →
∑ n ∈ t, invTotient n < ε := by
classical
have hs : Summable ((Nat.factoredNumbers s).indicator invTotient) :=
summable_subtype_iff_indicator.mp (summable_invTotient_factored s)
obtain ⟨t₀, ht₀⟩ := summable_iff_vanishing_norm.mp hs ε hε
refine ⟨t₀.sup id, fun t ht htR => ?_⟩
have hdis : Disjoint t t₀ := by
apply Finset.disjoint_left.mpr
intro n hnt hn₀
exact (not_lt_of_ge (Finset.le_sup (f := id) hn₀)) (htR n hnt)
have hbound := ht₀ t hdis
have hsum : (∑ n ∈ t, (Nat.factoredNumbers s).indicator invTotient n) =
∑ n ∈ t, invTotient n := by
apply Finset.sum_congr rfl
intro n hn
exact Set.indicator_of_mem (ht n hn) _
rw [hsum, Real.norm_eq_abs, abs_of_nonneg
(Finset.sum_nonneg fun n _ => invTotient_nonneg n)] at hbound
exact hbound
/- Original line 253: Erdos416Proof.bounded_prime_tail -/
theorem bounded_prime_tail {P : ℕ} (hP : 1 ≤ P) {ε : ℝ} (hε : 0 < ε) :
∃ R : ℕ, ∀ t : Finset ℕ,
(∀ n ∈ t, 0 < n ∧ largestPrimeFactor n ≤ P) →
(∀ n ∈ t, R < n) →
∑ n ∈ t, (n.totient : ℝ)⁻¹ < ε := by
obtain ⟨R, hR⟩ := invTotient_factored_tail (Finset.range (P + 1)) hε
refine ⟨R, fun t ht htR => hR t ?_ htR⟩
intro n hn
exact (mem_factored_range_iff hP).mpr (ht n hn)
/- Finite witness assignment used before the collision sieve. -/
/- Original line 265: Erdos416Proof.HasPeer -/
def HasPeer {α β : Type*} (f : α → β) (a : α) : Prop :=
∃ b, f b = f a ∧ b ≠ a
/- Original line 268: Erdos416Proof.exists_fiber_permutation -/
theorem exists_fiber_permutation {α β : Type*} [Fintype α] (f : α → β) :
∃ π : Equiv.Perm α, (∀ a, f (π a) = f a) ∧
∀ a, HasPeer f a → π a ≠ a := by
classical
have hfib : ∀ b : β, ∃ σ : Equiv.Perm {a : α // f a = b},
∀ x y, x ≠ y → σ x ≠ x := by
intro b
obtain ⟨σ, hσ, _⟩ :=
(Finset.univ : Finset {a : α // f a = b}).exists_cycleOn
refine ⟨σ, fun x y hxy => hσ.apply_ne ?_ (by simp)⟩
exact ⟨x, by simp, y, by simp, hxy⟩
choose σ hσ using hfib
let e := Equiv.sigmaFiberEquiv f
let π : Equiv.Perm α := e.symm.trans ((Equiv.sigmaCongrRight σ).trans e)
refine ⟨π, ?_, ?_⟩
· intro a
change f (σ (f a) ⟨a, rfl⟩).val = f a
exact (σ (f a) ⟨a, rfl⟩).property
· intro a ⟨b, hfb, hba⟩ hπ
have hne : (⟨a, rfl⟩ : {a' : α // f a' = f a}) ≠ ⟨b, hfb⟩ := by
intro h
exact hba (congrArg Subtype.val h).symm
apply hσ (f a) ⟨a, rfl⟩ ⟨b, hfb⟩ hne
apply Subtype.ext
exact hπ
/-- Cyclic witnesses on nonsingleton fibres and arbitrary witnesses on singleton
fibres can be combined without losing injectivity. -/
/- Original line 296: Erdos416Proof.exists_injective_witness -/
theorem exists_injective_witness {α β γ : Type*} [Fintype α]
(f : α → β) (g : γ → β) (canonical : α → γ)
(hcanonical : Function.Injective canonical)
(hvalue : ∀ a, g (canonical a) = f a)
(relation : α → γ → Prop)
(hpeer : ∀ a b, f b = f a → b ≠ a → relation a (canonical b))
(hwitness : ∀ a, ∃ z, g z = f a ∧ relation a z) :
∃ w : α → γ, Function.Injective w ∧
(∀ a, g (w a) = f a ∧ relation a (w a)) ∧
∀ a, HasPeer f a → ∃ b, w a = canonical b := by
classical
obtain ⟨π, hπvalue, hπmove⟩ := exists_fiber_permutation f
choose initial hinitialValue hinitialRel using hwitness
let w : α → γ := fun a =>
if HasPeer f a then canonical (π a) else initial a
have hwvalue (a : α) : g (w a) = f a := by
by_cases ha : HasPeer f a
· simp only [w, if_pos ha, hvalue, hπvalue]
· simp only [w, if_neg ha, hinitialValue]
refine ⟨w, ?_, ?_, ?_⟩
· intro a b hab
by_cases heq : a = b
· exact heq
have hfab : f a = f b := by rw [← hwvalue a, ← hwvalue b, hab]
have ha : HasPeer f a := ⟨b, hfab.symm, Ne.symm heq⟩
have hb : HasPeer f b := ⟨a, hfab, heq⟩
apply π.injective
apply hcanonical
simpa only [w, if_pos ha, if_pos hb] using hab
· intro a
refine ⟨hwvalue a, ?_⟩
by_cases ha : HasPeer f a
· simpa only [w, if_pos ha] using hpeer a (π a) (hπvalue a) (hπmove a ha)
· simpa only [w, if_neg ha] using hinitialRel a
· intro a ha
exact ⟨π a, by simp only [w, if_pos ha]⟩
/- Original line 333: Erdos416Proof.value_injective_on_singleton_fibres -/
theorem value_injective_on_singleton_fibres {α β : Type*} (f : α → β) :
Set.InjOn f {a | ¬ HasPeer f a} := by
intro a ha b _ hab
by_contra hne
exact ha ⟨b, hab.symm, Ne.symm hne⟩
open scoped Classical in
/- Original line 340: Erdos416Proof.collisionPoints -/
noncomputable def collisionPoints {α β : Type*} (s : Finset α) (f : α → β) :
Finset α :=
s.filter fun a => ∃ b ∈ s, b ≠ a ∧ f b = f a
/- Original line 344: Erdos416Proof.injective_off_collisionPoints -/
theorem injective_off_collisionPoints {α β : Type*} (s : Finset α) (f : α → β) :
Set.InjOn f ↑(s \ collisionPoints s f) := by
classical
intro a ha b hb hab
simp only [Finset.mem_coe, Finset.mem_sdiff] at ha hb
by_contra hne
apply ha.2
exact Finset.mem_filter.mpr ⟨ha.1, b, hb.1, Ne.symm hne, hab.symm⟩
/- Original line 353: Erdos416Proof.card_le_of_injective_off_bad -/
theorem card_le_of_injective_off_bad {α β : Type*}
(s bad : Finset α) (t : Finset β) (f : α → β)
(hmap : ∀ a ∈ s, f a ∈ t) (hinj : Set.InjOn f ↑(s \ bad)) :
s.card ≤ t.card + bad.card := by
classical
have hgood : (s \ bad).card ≤ t.card := by
apply Finset.card_le_card_of_injOn f ?_ hinj
intro a ha
exact hmap a (Finset.mem_sdiff.mp ha).1
have hpart := Finset.card_sdiff_add_card_inter s bad
have hbad : (s ∩ bad).card ≤ bad.card := Finset.card_le_card Finset.inter_subset_right
omega
open MeasureTheory
open scoped Pointwise
/- Original line 371: Erdos416Proof.one_sub_pow_le -/
theorem one_sub_pow_le (n : ℕ) {t : ℝ} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) :
1 - t ^ n ≤ n * (1 - t) := by
induction n with
| zero => simp
| succ n ih =>
have hp : t ^ n ≤ 1 := pow_le_one₀ ht₀ ht₁
have hterm : t ^ n * (1 - t) ≤ 1 - t :=
mul_le_of_le_one_left (sub_nonneg.mpr ht₁) hp
rw [pow_succ, Nat.cast_add, Nat.cast_one]
nlinarith
/- Original line 382: Erdos416Proof.volume_real_smul_nonneg -/
theorem volume_real_smul_nonneg {L : ℕ} {t : ℝ} (ht : 0 ≤ t)
(K : Set (Fin L → ℝ)) :
volume.real (t • K) = t ^ L * volume.real K := by
simp only [measureReal_def, Measure.addHaar_smul_of_nonneg volume ht,
Module.finrank_pi, Fintype.card_fin, ENNReal.toReal_mul,
ENNReal.toReal_ofReal (pow_nonneg ht L)]
/-- The part of a convex body above a linear cutoff avoids an inner dilation. -/
/- Original line 390: Erdos416Proof.outer_shell_volume -/
theorem outer_shell_volume {L : ℕ} (K : Set (Fin L → ℝ))
(hK : IsCompact K) (hconv : Convex ℝ K) (hzero : 0 ∈ K)
(A : (Fin L → ℝ) →ₗ[ℝ] ℝ) {b c t : ℝ}
(ht₀ : 0 ≤ t) (ht₁ : t ≤ 1)
(hbound : ∀ x ∈ K, A x ≤ b) (hcut : t * b ≤ c) :
volume.real (K ∩ {x | c < A x}) ≤ (1 - t ^ L) * volume.real K := by
have hscaled : t • K ⊆ K := by
rintro x ⟨y, hy, rfl⟩
exact hconv.smul_mem_of_zero_mem hzero hy ⟨ht₀, ht₁⟩
have hcompact : IsCompact (t • K) :=
hK.image (continuous_id.const_smul t)
have hfinite : volume K ≠ ⊤ := hK.measure_lt_top.ne
have hshell : K ∩ {x | c < A x} ⊆ K \ (t • K) := by
rintro x ⟨hx, hcx⟩
refine ⟨hx, ?_⟩
rintro ⟨z, hz, rfl⟩
have hzbound := (mul_le_mul_of_nonneg_left (hbound z hz) ht₀).trans hcut
simp only [Set.mem_ofPred_eq, map_smul, smul_eq_mul] at hcx
exact not_lt_of_ge hzbound hcx
calc
volume.real (K ∩ {x | c < A x}) ≤ volume.real (K \ (t • K)) :=
measureReal_mono hshell (measure_ne_top_of_subset Set.sdiff_subset hfinite)
_ = volume.real K - volume.real (t • K) :=
measureReal_sdiff hscaled hcompact.measurableSet hfinite
_ = (1 - t ^ L) * volume.real K := by
rw [volume_real_smul_nonneg ht₀]
ring
/- Original line 418: Erdos416Proof.outer_shell_volume_linear -/
theorem outer_shell_volume_linear {L : ℕ} (K : Set (Fin L → ℝ))
(hK : IsCompact K) (hconv : Convex ℝ K) (hzero : 0 ∈ K)
(A : (Fin L → ℝ) →ₗ[ℝ] ℝ) {b c t : ℝ}
(ht₀ : 0 ≤ t) (ht₁ : t ≤ 1)
(hbound : ∀ x ∈ K, A x ≤ b) (hcut : t * b ≤ c) :
volume.real (K ∩ {x | c < A x}) ≤ L * (1 - t) * volume.real K :=
(outer_shell_volume K hK hconv hzero A ht₀ ht₁ hbound hcut).trans
(mul_le_mul_of_nonneg_right (one_sub_pow_le L ht₀ ht₁) (measureReal_nonneg))
/-- Explicit form of the shell estimate, including thickening in an arbitrary
compact convex symmetric-error set. -/
/- Original line 429: Erdos416Proof.thickened_outer_shell_volume -/
theorem thickened_outer_shell_volume {L : ℕ} (hL : 1 ≤ L)
(E D : Set (Fin L → ℝ)) (hE : IsCompact E) (hD : IsCompact D)
(hconvE : Convex ℝ E) (hconvD : Convex ℝ D)
(hzeroE : 0 ∈ E) (hzeroD : 0 ∈ D)
(A : (Fin L → ℝ) →ₗ[ℝ] ℝ) {ξ δ η : ℝ}
(hξ : 1 ≤ ξ) (hδ : 0 ≤ δ) (hη : 0 ≤ η)
(hbound : ∀ x ∈ E, A x ≤ ξ)
(herror : ∀ z ∈ D, |A z| ≤ η) :
volume.real ((E ∩ {x | 1 - δ < A x}) + D) ≤
2 * L * (δ + ξ - 1 + η) * volume.real (E + D) := by
let K := E + D
have hcompact : IsCompact K := hE.add hD
have hconv : Convex ℝ K := hconvE.add hconvD
have hzero : 0 ∈ K := by
simpa only [zero_add] using Set.add_mem_add hzeroE hzeroD
have hfinite : volume K ≠ ⊤ := hcompact.measure_lt_top.ne
have hKbound : ∀ x ∈ K, A x ≤ ξ + η := by
rintro x ⟨u, hu, z, hz, rfl⟩
rw [map_add]
exact add_le_add (hbound u hu) (abs_le.mp (herror z hz)).2
have hshell : (E ∩ {x | 1 - δ < A x}) + D ⊆
K ∩ {x | 1 - δ - η < A x} := by
rintro x ⟨u, ⟨hu, hAu⟩, z, hz, rfl⟩
refine ⟨Set.add_mem_add hu hz, ?_⟩
change 1 - δ - η < A (u + z)
rw [map_add]
have hzlower := (abs_le.mp (herror z hz)).1
change 1 - δ < A u at hAu
linarith
have hsubset : (E ∩ {x | 1 - δ < A x}) + D ⊆ K :=
hshell.trans Set.inter_subset_left
have hnonneg : 0 ≤ volume.real K := measureReal_nonneg
have hLreal : (1 : ℝ) ≤ L := by exact_mod_cast hL
have htotal : 0 ≤ δ + ξ - 1 + η := by linarith
by_cases hc : 0 < 1 - δ - η
· have hb : 0 < ξ + η := by linarith
let t := (1 - δ - η) / (ξ + η)
have ht₀ : 0 ≤ t := (div_pos hc hb).le
have ht₁ : t ≤ 1 := (div_le_one hb).mpr (by linarith)
have hcut : t * (ξ + η) ≤ 1 - δ - η := by
exact le_of_eq (div_mul_cancel₀ _ hb.ne')
have hwidth : 1 - t ≤ 2 * (δ + ξ - 1 + η) := by
have htprod : t * (ξ + η) = 1 - δ - η :=
div_mul_cancel₀ _ hb.ne'
have hb₁ : 1 ≤ ξ + η := by linarithProvenance