OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWindowSubstitution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conversion of relative additive windows to the logarithmic window, including the physical-variable Jacobian.

  1. lemma OAI.TwoPointCorrelations.mrt_log_window_measurable line 14
  2. lemma OAI.TwoPointCorrelations.mrt_relative_interval_identity line 22
  3. lemma OAI.TwoPointCorrelations.mrt_relative_interval_sq line 34
  4. lemma OAI.TwoPointCorrelations.mrt_log_weight_integral_bound line 41
  5. theorem OAI.TwoPointCorrelations.mrt_relative_window_energy line 82