IndisputableMonolith.ILG.XiBins

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace ILG
   5
   6noncomputable section
   7open Real
   8
   9/-! Dependency-light ILG helpers: n_of_r and xi_of_bin. -/
  10
  11@[simp] def εr : ℝ := 1e-12
  12
  13/-- Analytic global radial shape factor n(r) = 1 + A (1 - exp(-(r/r0)^p)). -/
  14@[simp] noncomputable def n_of_r (A r0 p : ℝ) (r : ℝ) : ℝ :=
  15  let x := (max 0 r) / max εr r0
  16  1 + A * (1 - Real.exp (-(x ^ p)))
  17
  18/-- Monotonicity in A under nonnegative exponent. -/
  19lemma n_of_r_mono_A_of_nonneg_p {A1 A2 r0 p r : ℝ}
  20  (hp : 0 ≤ p) (hA12 : A1 ≤ A2) :
  21  n_of_r A1 r0 p r ≤ n_of_r A2 r0 p r := by
  22  dsimp [n_of_r]
  23  set x := (max 0 r) / max εr r0 with hx
  24  have hden_pos : 0 < max εr r0 := by
  25    have : 0 < εr := by
  26      have : (1e-12 : ℝ) > 0 := by norm_num
  27      simpa [εr] using this
  28    exact lt_max_of_lt_left this
  29  have hbase_nonneg : 0 ≤ (max 0 r) / max εr r0 := by
  30    have : 0 ≤ max 0 r := le_max_left _ _
  31    exact div_nonneg this (le_of_lt hden_pos)
  32  have hx_nonneg : 0 ≤ x := by simpa [hx] using hbase_nonneg
  33  have hx_pow_nonneg : 0 ≤ x ^ p := Real.rpow_nonneg hx_nonneg hp
  34  have hterm_nonneg : 0 ≤ 1 - Real.exp (-(x ^ p)) := by
  35    have : Real.exp (-(x ^ p)) ≤ 1 := by
  36      have : -(x ^ p) ≤ 0 := by exact neg_nonpos.mpr hx_pow_nonneg
  37      exact Real.exp_le_one_of_nonpos this
  38    exact sub_nonneg.mpr this
  39  have : A1 * (1 - Real.exp (-(x ^ p))) ≤ A2 * (1 - Real.exp (-(x ^ p))) :=
  40    mul_le_mul_of_nonneg_right hA12 hterm_nonneg
  41  simpa [hx, add_comm, add_left_comm, add_assoc]
  42    using add_le_add_left this 1
  43
  44/-- Threads-informed global factor ξ from bin-center u ∈ [0,1]. -/
  45@[simp] noncomputable def xi_of_u (u : ℝ) : ℝ := 1 + Real.sqrt (max 0 (min 1 u))
  46
  47/-- Deterministic bin centers for global-only ξ (quintiles). -/
  48@[simp] noncomputable def xi_of_bin : Nat → ℝ
  49| 0 => xi_of_u 0.1
  50| 1 => xi_of_u 0.3
  51| 2 => xi_of_u 0.5
  52| 3 => xi_of_u 0.7
  53| _ => xi_of_u 0.9
  54
  55/-- Monotonicity over the canonical quintile bin centers. -/
  56lemma xi_of_bin_mono : xi_of_bin 0 ≤ xi_of_bin 1 ∧ xi_of_bin 1 ≤ xi_of_bin 2 ∧
  57  xi_of_bin 2 ≤ xi_of_bin 3 ∧ xi_of_bin 3 ≤ xi_of_bin 4 := by
  58  -- xi_of_u is monotone in u on [0,1] because sqrt and max/min are monotone
  59  have mono_xi : Monotone xi_of_u := by
  60    intro u v huv
  61    dsimp [xi_of_u]
  62    have hclamp : max 0 (min 1 u) ≤ max 0 (min 1 v) := by
  63      exact max_le_max (le_of_eq rfl) (min_le_min_right (le_of_lt ?_))
  64    -- Provide a simple bound using basic facts: since 0 ≤ max 0 (min 1 u) ≤ max 0 (min 1 v)
  65    -- and sqrt is monotone on ℝ≥0
  66    have h0u : 0 ≤ max 0 (min 1 u) := le_max_left _ _
  67    have h0v : 0 ≤ max 0 (min 1 v) := le_max_left _ _
  68    have hsqrt := Real.sqrt_le_sqrt_iff.mpr hclamp
  69    exact add_le_add_left hsqrt 1
  70  have h01 : (0 : ℝ) ≤ 0.1 := by norm_num
  71  have h12 : (0.1 : ℝ) ≤ 0.3 := by norm_num
  72  have h23 : (0.3 : ℝ) ≤ 0.5 := by norm_num
  73  have h34 : (0.5 : ℝ) ≤ 0.7 := by norm_num
  74  have h45 : (0.7 : ℝ) ≤ 0.9 := by norm_num
  75  have h0 := mono_xi (by exact h12)
  76  have h1 := mono_xi (by exact h23)
  77  have h2 := mono_xi (by exact h34)
  78  have h3 := mono_xi (by exact h45)
  79  dsimp [xi_of_bin] at h0 h1 h2 h3
  80  exact And.intro h0 (And.intro h1 (And.intro h2 h3))
  81
  82end
  83end ILG
  84end IndisputableMonolith
  85