FiniteVolumeProfile

formal source

  36The field `finiteVolumeControl` is the finite-volume norm-equivalence input:
  37on a finite lattice, pointwise amplitude is controlled by `sqrt(siteCount)` times
  38the RMS scale. -/
  39structure FiniteVolumeProfile where
  40  siteCount : ℕ
  41  siteCount_pos : 0 < siteCount
  42  omegaMax : ℝ
  43  omegaRms : ℝ
  44  omegaRms_pos : 0 < omegaRms
  45  omegaRms_le_max : omegaRms ≤ omegaMax
  46  finiteVolumeControl : omegaMax ≤ Real.sqrt siteCount * omegaRms
  47
  48/-- The normalized ratio used by the lattice FRC bridge. -/
  49def normalizedRatio (s : FiniteVolumeProfile) : ℝ :=
  50  s.omegaMax / s.omegaRms
  51
  52theorem normalizedRatio_pos (s : FiniteVolumeProfile) : 0 < normalizedRatio s := by
  53  unfold normalizedRatio
  54  exact div_pos (lt_of_lt_of_le s.omegaRms_pos s.omegaRms_le_max) s.omegaRms_pos
  55
  56theorem normalizedRatio_ge_one (s : FiniteVolumeProfile) : 1 ≤ normalizedRatio s := by
  57  unfold normalizedRatio
  58  exact (one_le_div s.omegaRms_pos).2 s.omegaRms_le_max
  59
  60theorem normalizedRatio_le_sqrt_siteCount (s : FiniteVolumeProfile) :
  61    normalizedRatio s ≤ Real.sqrt s.siteCount := by
  62  unfold normalizedRatio
  63  rw [div_le_iff₀ s.omegaRms_pos]
  64  simpa [mul_comm, mul_left_comm, mul_assoc] using s.finiteVolumeControl
  65
  66/-! ## Bounding J-cost on the lattice -/
  67
  68/-- On the half-line `[1, ∞)`, the canonical cost is bounded by the identity.
  69