import MaxLeafFormal.RSCover0
import MaxLeafFormal.RSCover1
import MaxLeafFormal.RSCover2
import MaxLeafFormal.RSCover3
import MaxLeafFormal.RSCover4
import MaxLeafFormal.RSCover5
import MaxLeafFormal.RSCover6
import MaxLeafFormal.RSCover7
import MaxLeafFormal.RSCover8
import MaxLeafFormal.RSCover9
import MaxLeafFormal.RSCover10
import MaxLeafFormal.RSCover11
import MaxLeafFormal.RSCover12
import MaxLeafFormal.RSCover13
import MaxLeafFormal.RSCover14
import MaxLeafFormal.RSCover15
import MaxLeafFormal.RSCover16
import MaxLeafFormal.RSCover17
import MaxLeafFormal.RSCover18
import MaxLeafFormal.RSCover19
import MaxLeafFormal.RSCover20
import MaxLeafFormal.RSCover21

/-!
# RS: the closed-form rate (`prop:rs-rate`(c)) and the constants of `thm:rs`

`F*(1) = 0` and the identification of `eq:rs-F` with `F*` of `eq:co-Fstar` for `β = 1`,
`ρ = 1/σ`; (c) `F*(σ) ≤ log 1.744835` on `(0, 1]`, `F*(σ) ≤ 0.7807` on `(0, 0.31]`,
`F*(σ) ≤ 0.7802` on `[0.54, 1]`; and `ω_RS = 0.80309062 > log 1.744835`,
`2^{ω_RS} = 1.744835… < 1.7449` (proof of `thm:rs`).

The interval covers are the generated modules `RSCover0` … `RSCover21`
(`scripts/export_rs_cover.py`): chunks 0–19 cover `[1/5, 4/5]` for the target
`0.8030906143 < log 1.744835`, chunk 20 covers `[0.15, 0.31]` for `0.7807`, chunk 21 covers
`[0.54, 0.8]` for `0.7802`. Outside `[1/5, 4/5]`, `F* ≤ H ≤ H(1/5) < 0.73` (proof of (c)), with
`H(1/5)` enclosed by `Enclose.H2Q`.
-/

namespace MaxLeafFormal.RSRate

open Enclose

theorem rsF_one : rsF 1 = 0 := by
  simp [rsF, MLS.H2]

/-- `x < 2 ^ x` for `x ≥ 0`. -/
theorem lt_two_rpow {x : ℝ} (hx : 0 ≤ x) : x < (2:ℝ) ^ x := by
  set n := ⌊x⌋₊ with hn
  have h1 : x < (n : ℝ) + 1 := Nat.lt_floor_add_one x
  have h2 : ((n + 1 : ℕ) : ℝ) ≤ ((2 ^ n : ℕ) : ℝ) := by exact_mod_cast Nat.lt_two_pow_self
  have h3 : (2:ℝ) ^ (n : ℝ) ≤ (2:ℝ) ^ x :=
    Real.rpow_le_rpow_of_exponent_le (by norm_num) (Nat.floor_le hx)
  rw [Real.rpow_natCast] at h3
  push_cast at h2
  linarith

theorem rsF_eq_Fstar {σ : ℝ} (hσ : σ ∈ Set.Ioo (0:ℝ) 1) : rsF σ = MLS.Fstar σ 1 σ⁻¹ := by
  obtain ⟨h0, h1⟩ := hσ
  have hlt : (2:ℝ) ^ (-σ⁻¹) < σ := by
    have hpos : (0:ℝ) < (2:ℝ) ^ σ⁻¹ := Real.rpow_pos_of_pos (by norm_num) _
    have key := lt_two_rpow (inv_pos.mpr h0).le
    rw [Real.rpow_neg (by norm_num), inv_lt_comm₀ hpos h0]
    exact key
  unfold MLS.Fstar rsF
  rw [show -1 / σ = -σ⁻¹ by ring]
  split_ifs with h
  · exact absurd h (not_le.mpr hlt)
  · rw [mul_inv_cancel₀ h0.ne']
    ring

/-- `F* ≤ H` on `(0, 1)`. -/
theorem rsF_le_H2 {σ : ℝ} (h0 : 0 < σ) (h1 : σ < 1) : rsF σ ≤ MLS.H2 σ := by
  have hp0 : (0:ℝ) ≤ (2:ℝ) ^ (-1 / σ) := Real.rpow_nonneg (by norm_num) _
  have hp1 : (2:ℝ) ^ (-1 / σ) ≤ 1 :=
    Real.rpow_le_one_of_one_le_of_nonpos (by norm_num) (by rw [neg_div]; exact neg_nonpos.mpr (by positivity))
  have hl : Real.logb 2 (1 - (2:ℝ) ^ (-1 / σ)) ≤ 0 :=
    Real.logb_nonpos (by norm_num) (by linarith) (by linarith)
  unfold rsF
  nlinarith

/-- `H(1/5) < 0.73`. -/
theorem H2_fifth : MLS.H2 (1 / 5) < 73 / 100 := by
  have h := (H2Q_sound (x := 1 / 5) (by norm_num) (by norm_num) 40 48).2
  have hc : (H2Q (1 / 5) 40 48).hi < 73 / 100 := by decide +kernel
  have hc' : (((H2Q (1 / 5) 40 48).hi : ℚ) : ℝ) < ((73 / 100 : ℚ) : ℝ) := by exact_mod_cast hc
  push_cast at h hc'
  linarith

/-- Outside `[1/5, 4/5]`: `F*(σ) ≤ H(σ) ≤ H(1/5) < 0.73`. -/
theorem rsF_outside {σ : ℝ} (h0 : 0 < σ) (h1 : σ < 1) (h : σ ≤ 1 / 5 ∨ 4 / 5 ≤ σ) :
    rsF σ < 73 / 100 := by
  have hH : MLS.H2 σ ≤ MLS.H2 (1 / 5) := by
    unfold MLS.H2
    have hlog2 : 0 < Real.log 2 := Real.log_pos (by norm_num)
    apply div_le_div_of_nonneg_right _ hlog2.le
    rcases h with h | h
    · exact Real.binEntropy_strictMonoOn.monotoneOn ⟨h0.le, by linarith⟩
        ⟨by norm_num, by norm_num⟩ h
    · rw [← Real.binEntropy_one_sub σ]
      exact Real.binEntropy_strictMonoOn.monotoneOn ⟨by linarith, by linarith⟩
        ⟨by norm_num, by norm_num⟩ (by linarith)
  linarith [rsF_le_H2 h0 h1, H2_fifth]

/-- Constants for the proof of `thm:rs`. -/
theorem rs_constants :
    Real.logb 2 (1744835/10^6) < 80309062/10^8 ∧
    (1744835/10^6 : ℝ) ≤ (2:ℝ) ^ (80309062/10^8 : ℝ) ∧ (2:ℝ) ^ (80309062/10^8 : ℝ) < 1744836/10^6 := by
  have hL := (log2Q_sound (q := 1744835 / 10 ^ 6) (by norm_num) 50 64).2
  have hc1 : (log2Q (1744835 / 10 ^ 6) 50 64).hi < 80309062 / 10 ^ 8 := by decide +kernel
  have hP := pow2Q_sound (80309062 / 10 ^ 8) 50 64
  have hc2 : 1744835 / 10 ^ 6 ≤ (pow2Q (80309062 / 10 ^ 8) 50 64).lo := by decide +kernel
  have hc3 : (pow2Q (80309062 / 10 ^ 8) 50 64).hi < 1744836 / 10 ^ 6 := by decide +kernel
  have hc1' : (((log2Q (1744835 / 10 ^ 6) 50 64).hi : ℚ) : ℝ) < ((80309062 / 10 ^ 8 : ℚ) : ℝ) := by
    exact_mod_cast hc1
  have hc2' : ((1744835 / 10 ^ 6 : ℚ) : ℝ) ≤ (((pow2Q (80309062 / 10 ^ 8) 50 64).lo : ℚ) : ℝ) := by
    exact_mod_cast hc2
  have hc3' : (((pow2Q (80309062 / 10 ^ 8) 50 64).hi : ℚ) : ℝ) < ((1744836 / 10 ^ 6 : ℚ) : ℝ) := by
    exact_mod_cast hc3
  obtain ⟨hP1, hP2⟩ := hP
  push_cast at hL hc1' hc2' hc3' hP1 hP2
  exact ⟨by linarith, by linarith, by linarith⟩

/-- The target of cover 1 lies below `log 1.744835`. -/
theorem T1_lt : ((q 8030906143 10000000000 : ℚ) : ℝ) < Real.logb 2 (1744835/10^6) := by
  have hL := (log2Q_sound (q := 1744835 / 10 ^ 6) (by norm_num) 50 64).1
  have hc : q 8030906143 10000000000 < (log2Q (1744835 / 10 ^ 6) 50 64).lo := by
    unfold q; decide +kernel
  have hc' : ((q 8030906143 10000000000 : ℚ) : ℝ) < (((log2Q (1744835 / 10 ^ 6) 50 64).lo : ℚ) : ℝ) := by
    exact_mod_cast hc
  push_cast at hL hc' ⊢
  linarith


theorem Icc_join {P : ℝ → Prop} {a b c : ℝ} (h1 : ∀ σ ∈ Set.Icc a b, P σ)
    (h2 : ∀ σ ∈ Set.Icc b c, P σ) : ∀ σ ∈ Set.Icc a c, P σ := by
  intro σ hσ
  rcases le_total σ b with h | h
  · exact h1 σ ⟨hσ.1, h⟩
  · exact h2 σ ⟨h, hσ.2⟩

/-- Cover 1: `F* ≤ 0.8030906143` on `[1/5, 4/5]`. -/
theorem cover_one : ∀ σ ∈ Set.Icc ((q 1 5 : ℚ) : ℝ) ((q 4 5 : ℚ) : ℝ),
    rsF σ ≤ ((q 8030906143 10000000000 : ℚ) : ℝ) :=
  Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (Icc_join (cover0_sound) cover1_sound) cover2_sound) cover3_sound) cover4_sound) cover5_sound) cover6_sound) cover7_sound) cover8_sound) cover9_sound) cover10_sound) cover11_sound) cover12_sound) cover13_sound) cover14_sound) cover15_sound) cover16_sound) cover17_sound) cover18_sound) cover19_sound

theorem rs_rate_c :
    (∀ σ ∈ Set.Ioc (0:ℝ) 1, rsF σ ≤ Real.logb 2 (1744835/10^6)) ∧
    (∀ σ ∈ Set.Ioc (0:ℝ) (31/100), rsF σ ≤ 7807/10^4) ∧
    (∀ σ ∈ Set.Icc (54/100 : ℝ) 1, rsF σ ≤ 7802/10^4) := by
  have hT1 := T1_lt
  have hq : ∀ a b : ℕ, ((q a b : ℚ) : ℝ) = (a : ℝ) / b := fun a b => by unfold q; push_cast; rfl
  have c1 := cover_one
  have c2 := cover20_sound
  have c3 := cover21_sound
  simp only [hq] at c1 c2 c3 hT1
  norm_num at c1 c2 c3 hT1
  refine ⟨?_, ?_, ?_⟩
  · rintro σ ⟨h0, h1⟩
    rcases h1.lt_or_eq with h1 | rfl
    · by_cases hin : 1 / 5 ≤ σ ∧ σ ≤ 4 / 5
      · linarith [c1 σ (by linarith [hin.1]) (by linarith [hin.2])]
      · have := rsF_outside h0 h1 (by
          rcases not_and_or.mp hin with h | h
          · exact Or.inl (by linarith [not_le.mp h])
          · exact Or.inr (by linarith [not_le.mp h]))
        linarith
    · rw [rsF_one]; linarith
  · rintro σ ⟨h0, h1⟩
    by_cases hin : 15 / 100 ≤ σ
    · exact (c2 σ (by linarith) (by linarith)).trans (by norm_num)
    · have := rsF_outside h0 (by linarith) (Or.inl (by linarith [not_le.mp hin]))
      linarith
  · rintro σ ⟨h0, h1⟩
    rcases h1.lt_or_eq with h1 | rfl
    · by_cases hin : σ ≤ 4 / 5
      · exact (c3 σ (by linarith) (by linarith)).trans (by norm_num)
      · have := rsF_outside (by linarith) h1 (Or.inr (by linarith [not_le.mp hin]))
        linarith
    · rw [rsF_one]; norm_num

end MaxLeafFormal.RSRate