import Erdos1135.Tao.Section3.AmbientGeometricBudget

/-!
# Section 3 Forward-Window Multiplicity

Adjacent inclusive forward windows may share a rounded endpoint.  Windows of
the same index parity are strictly separated, so the full family has
multiplicity at most two.  This leaf retains the stronger odd-prefix
normalization needed by the later exact `v₂` transfer.
-/

namespace Erdos1135
namespace Tao

open scoped BigOperators

noncomputable section

/-- Set view of the `m`-th seed-forward odd window. -/
def taoSection3ForwardWindowSet (y : ℝ) (m : ℕ) : Set ℕ :=
  oddLogWindowSet
    (taoNyLo (taoSection3ForwardScale y m))
    (taoNyHi (taoSection3ForwardScale y m) taoAlpha)

theorem taoSection3ForwardScale_strictMono
    {y : ℝ} (hy : 1 < y) :
    StrictMono (taoSection3ForwardScale y) := by
  simpa only [taoSection3ForwardScale, Function.comp_apply] using
    (Real.strictMono_rpow_of_base_gt_one hy).comp
      (pow_right_strictMono₀ taoAlpha_one_lt)

theorem taoSection3ForwardWindow_hi_eq_floor_next
    {y : ℝ} (hy : 0 ≤ y) (m : ℕ) :
    taoNyHi (taoSection3ForwardScale y m) taoAlpha =
      Nat.floor (taoSection3ForwardScale y (m + 1)) := by
  unfold taoNyHi
  rw [taoSection3ForwardScale_succ hy]

theorem taoSection3ForwardWindow_hi_lt_lo_of_add_two_le
    {y : ℝ} (hy : 1 < y) {m n : ℕ} (hmn : m + 2 ≤ n) :
    taoNyHi (taoSection3ForwardScale y m) taoAlpha <
      taoNyLo (taoSection3ForwardScale y n) := by
  rw [taoSection3ForwardWindow_hi_eq_floor_next
    (zero_le_one.trans hy.le)]
  unfold taoNyLo
  apply Nat.floor_lt_ceil_of_lt_of_pos
  · exact taoSection3ForwardScale_strictMono hy (by omega)
  · unfold taoSection3ForwardScale
    exact Real.rpow_pos_of_pos (zero_lt_one.trans hy) _

theorem taoSection3ForwardWindow_hi_le_top
    {y : ℝ} (hy : 1 ≤ y) {m L : ℕ} (hm : m < L) :
    taoNyHi (taoSection3ForwardScale y m) taoAlpha ≤
      Nat.floor (taoSection3ForwardScale y L) := by
  rw [taoSection3ForwardWindow_hi_eq_floor_next
    (zero_le_one.trans hy)]
  exact Nat.floor_mono
    (taoSection3ForwardScale_monotone hy (by omega))

theorem logCount_taoSection3ForwardWindowSet_eq_mass
    {y : ℝ} (hy : 1 ≤ y) {m L : ℕ} (hm : m < L) :
    logCount (taoSection3ForwardWindowSet y m)
        (Nat.floor (taoSection3ForwardScale y L)) =
      logFinsetMass (taoSection3ForwardWindow y m) := by
  calc
    logCount (taoSection3ForwardWindowSet y m)
        (Nat.floor (taoSection3ForwardScale y L)) =
        logCount (taoSection3ForwardWindowSet y m)
          (taoNyHi (taoSection3ForwardScale y m) taoAlpha) :=
      logCount_eq_of_subset_Iic_of_le
        (oddLogWindowSet_subset_Iic
          (taoNyLo (taoSection3ForwardScale y m))
          (taoNyHi (taoSection3ForwardScale y m) taoAlpha))
        (taoSection3ForwardWindow_hi_le_top hy hm)
    _ = logFinsetMass (taoSection3ForwardWindow y m) := by
      exact logCount_oddLogWindowSet_eq_logFinsetMass
        (taoNyLo (taoSection3ForwardScale y m))
        (taoNyHi (taoSection3ForwardScale y m) taoAlpha)

private theorem sum_logCount_forwardWindow_filter_le_oddPrefix
    {y : ℝ} (hy : 1 < y) (L : ℕ)
    (p : ℕ → Prop) [DecidablePred p]
    (hsep : ∀ {i j : ℕ}, i < L → j < L → p i → p j →
      i < j → i + 2 ≤ j) :
    (∑ m ∈ (Finset.range L).filter p,
      logCount (taoSection3ForwardWindowSet y m)
        (Nat.floor (taoSection3ForwardScale y L))) ≤
      logCount {n : ℕ | Odd n}
        (Nat.floor (taoSection3ForwardScale y L)) := by
  let I := (Finset.range L).filter p
  have hgap : ∀ i ∈ I, ∀ j ∈ I, i < j →
      taoNyHi (taoSection3ForwardScale y i) taoAlpha <
        taoNyLo (taoSection3ForwardScale y j) := by
    intro i hiI j hjI hij
    have hi := Finset.mem_filter.mp hiI
    have hj := Finset.mem_filter.mp hjI
    exact taoSection3ForwardWindow_hi_lt_lo_of_add_two_le hy
      (hsep (Finset.mem_range.mp hi.1) (Finset.mem_range.mp hj.1)
        hi.2 hj.2 hij)
  have hdisj : ∀ i ∈ I, ∀ j ∈ I, i ≠ j →
      Disjoint (taoSection3ForwardWindowSet y i)
        (taoSection3ForwardWindowSet y j) := by
    simpa only [taoSection3ForwardWindowSet] using
      (oddLogWindowSet_pairwise_disjoint_of_ordered_gaps I
        (fun m => taoNyLo (taoSection3ForwardScale y m))
        (fun m => taoNyHi (taoSection3ForwardScale y m) taoAlpha)
        hgap)
  rw [show (Finset.range L).filter p = I by rfl,
    ← logCount_biUnion_of_pairwise_disjoint I
      (taoSection3ForwardWindowSet y) hdisj]
  apply logCount_mono
  intro n hn
  rcases Set.mem_iUnion.mp hn with ⟨m, hn⟩
  rcases Set.mem_iUnion.mp hn with ⟨_hmI, hnWindow⟩
  exact Nat.odd_iff.mpr
    (oddLogWindowSet_mem.mp hnWindow).2.2

/-- The forward windows have logarithmic multiplicity at most two, with the
right side normalized by the odd prefix rather than the full prefix. -/
theorem sum_logFinsetMass_taoSection3ForwardWindow_le_two_logCount_odd
    {y : ℝ} (hy : 1 < y) (L : ℕ) :
    (∑ m ∈ Finset.range L,
      logFinsetMass (taoSection3ForwardWindow y m)) ≤
      2 * logCount {n : ℕ | Odd n}
        (Nat.floor (taoSection3ForwardScale y L)) := by
  classical
  have hevenSep : ∀ {i j : ℕ}, i < L → j < L → Even i → Even j →
      i < j → i + 2 ≤ j := by
    intro i j _hiL _hjL hi hj hij
    have hgap := Nat.add_one_lt_of_even hi hj hij
    omega
  have hoddSep : ∀ {i j : ℕ}, i < L → j < L → ¬ Even i → ¬ Even j →
      i < j → i + 2 ≤ j := by
    intro i j _hiL _hjL hi hj hij
    have hiOdd : Odd i := Nat.not_even_iff_odd.mp hi
    have hjOdd : Odd j := Nat.not_even_iff_odd.mp hj
    have hgap := Nat.add_one_lt_of_even hiOdd.add_one hjOdd.add_one (by omega)
    omega
  have heven := sum_logCount_forwardWindow_filter_le_oddPrefix
    hy L (fun m => Even m) hevenSep
  have hodd := sum_logCount_forwardWindow_filter_le_oddPrefix
    hy L (fun m => ¬ Even m) hoddSep
  calc
    (∑ m ∈ Finset.range L,
        logFinsetMass (taoSection3ForwardWindow y m)) =
        ∑ m ∈ Finset.range L,
          logCount (taoSection3ForwardWindowSet y m)
            (Nat.floor (taoSection3ForwardScale y L)) := by
      apply Finset.sum_congr rfl
      intro m hm
      exact (logCount_taoSection3ForwardWindowSet_eq_mass
        hy.le (Finset.mem_range.mp hm)).symm
    _ = (∑ m ∈ (Finset.range L).filter (fun m => Even m),
          logCount (taoSection3ForwardWindowSet y m)
            (Nat.floor (taoSection3ForwardScale y L))) +
        ∑ m ∈ (Finset.range L).filter (fun m => ¬ Even m),
          logCount (taoSection3ForwardWindowSet y m)
            (Nat.floor (taoSection3ForwardScale y L)) := by
      rw [← Finset.sum_filter_add_sum_filter_not
        (Finset.range L) (fun m : ℕ => Even m)
        (fun m => logCount (taoSection3ForwardWindowSet y m)
          (Nat.floor (taoSection3ForwardScale y L)))]
    _ ≤ logCount {n : ℕ | Odd n}
          (Nat.floor (taoSection3ForwardScale y L)) +
        logCount {n : ℕ | Odd n}
          (Nat.floor (taoSection3ForwardScale y L)) :=
      add_le_add heven hodd
    _ = 2 * logCount {n : ℕ | Odd n}
          (Nat.floor (taoSection3ForwardScale y L)) := by
      ring

/-- Starting from the ambient seed, the scale after all `j + 2` cover
windows is exactly the real ambient endpoint. -/
theorem taoSection3AmbientForwardScale_top
    {X : ℝ} (hX : 0 ≤ X) (j : ℕ) :
    taoSection3ForwardScale
        (taoSection3AmbientBoundary X (j + 2)) (j + 2) = X := by
  simpa only [Nat.zero_add, taoSection3AmbientBoundary, pow_zero,
    Real.rpow_one] using
    (taoSection3ForwardScale_ambient_add hX 0 (j + 2))

/-- At a natural ambient endpoint, every active window mass is already a
`logCount` at that common endpoint. -/
theorem logCount_taoSection3AmbientActiveWindowSet_eq_mass
    {X : ℕ} (hX : 1 ≤ X) (j : ℕ) {m : ℕ} (hm : m < j + 2) :
    logCount
        (taoSection3ForwardWindowSet
          (taoSection3AmbientBoundary (X : ℝ) (j + 2)) m) X =
      logFinsetMass
        (taoSection3ForwardWindow
          (taoSection3AmbientBoundary (X : ℝ) (j + 2)) m) := by
  have hy : 1 ≤ taoSection3AmbientBoundary (X : ℝ) (j + 2) :=
    taoSection3AmbientBoundary_one_le (by exact_mod_cast hX) (j + 2)
  have hmass := logCount_taoSection3ForwardWindowSet_eq_mass hy hm
  rw [taoSection3AmbientForwardScale_top (Nat.cast_nonneg X) j] at hmass
  simpa using hmass

/-- The active ambient cover has `j + 2` windows, although the preceding
passage-error trace has only `j + 1` calls. -/
theorem sum_logFinsetMass_taoSection3AmbientActiveWindow_le_two_logCount_odd
    {X : ℝ} (hX : 1 < X) (j : ℕ) :
    (∑ m ∈ Finset.range (j + 2),
      logFinsetMass
        (taoSection3ForwardWindow
          (taoSection3AmbientBoundary X (j + 2)) m)) ≤
      2 * logCount {n : ℕ | Odd n} (Nat.floor X) := by
  have hy : 1 < taoSection3AmbientBoundary X (j + 2) := by
    unfold taoSection3AmbientBoundary
    exact Real.one_lt_rpow hX
      (pow_pos taoSection3AmbientRatio_pos (j + 2))
  simpa only [taoSection3AmbientForwardScale_top
    (zero_le_one.trans hX.le) j] using
    (sum_logFinsetMass_taoSection3ForwardWindow_le_two_logCount_odd
      hy (j + 2))

theorem sum_logFinsetMass_taoSection3AmbientActiveWindow_nat_le_two_logCount_odd
    {X : ℕ} (hX : 1 < X) (j : ℕ) :
    (∑ m ∈ Finset.range (j + 2),
      logFinsetMass
        (taoSection3ForwardWindow
          (taoSection3AmbientBoundary (X : ℝ) (j + 2)) m)) ≤
      2 * logCount {n : ℕ | Odd n} X := by
  simpa using
    (sum_logFinsetMass_taoSection3AmbientActiveWindow_le_two_logCount_odd
      (X := (X : ℝ)) (by exact_mod_cast hX) j)

end

end Tao
end Erdos1135