-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyEntourage_le_log_coverMincard_div {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : SymmetricRel U) {n : ℕ} (n_pos : 0 < n) :
    coverEntropyEntourage T F (U ○ U) ≤ log (coverMincard T F U n) / n

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
have key : w ≤ᶠ[atTop] u + v :=
  eventually_atTop.2 ⟨1, fun m m_pos ↦ log_coverMincard_le_add F_inv U_symm n_pos m_pos⟩

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
let w := fun m : ℕ ↦ log (coverMincard T F (U ○ U) m) / m

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
⊢ limsup v atTop = 0

Tactic:
exact Tendsto.limsup_eq (EReal.tendsto_const_div_atTop_nhds_zero_nat logm_nneg logm_fin)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this : limsup (u + v) atTop ≤ limsup u atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
exact this.trans_eq (limsup_const (log (coverMincard T F U n) / n))

Result:
no goals

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
let u := fun _ : ℕ ↦ log (coverMincard T F U n) / n

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
let v := fun m : ℕ ↦ log (coverMincard T F U n) / m

Result:
case inr.inr
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_bot : (↑(coverMincard T F U n)).log = ⊥
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rw [log_eq_bot_iff, ← ENat.toENNReal_zero, ENat.toENNReal_inj,
  coverMincard_eq_zero_iff T F U n] at logm_bot

Result:
case inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_bot : F = ∅
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Proof state:
case inr.inl
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_top : (↑(coverMincard T F U n)).log = ⊤
⊢ coverEntropyEntourage T F (U ○ U) ≤ ⊤

Tactic:
exact le_top

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
have := @limsup_add_le ℕ atTop u v

Result:
X : Type u_1
T : X → X
F : Set X
F_inv : MapsTo T F F
U : Set (X × X)
U_symm : SymmetricRel U
n : ℕ
n_pos : 0 < n
logm_nneg : (↑(coverMincard T F U n)).log ≠ ⊥
logm_fin : (↑(coverMincard T F U n)).log ≠ ⊤
u : ℕ → EReal := fun x => (↑(coverMincard T F U n)).log / ↑n
v : ℕ → EReal := fun m => (↑(coverMincard T F U n)).log / ↑m
w : ℕ → EReal := fun m => (↑(coverMincard T F (U ○ U) m)).log / ↑m
key : w ≤ᶠ[atTop] u + v
h : limsup v atTop = 0
this :
  limsup u atTop ≠ ⊥ ∨ limsup v atTop ≠ ⊤ →
    limsup u atTop ≠ ⊤ ∨ limsup v atTop ≠ ⊥ → limsup (u + v) atTop ≤ limsup u atTop + limsup v atTop
⊢ limsup (u + v) atTop ≤ (↑(coverMincard T F U n)).log / ↑n