MRTBandCancellation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The elementary band cancellation in corrected MRT, Appendix A, Lemma A.8 and equation (A.12).

lemma OAI.TwoPointCorrelations.mrt_exp_sub_square_monotone line 15
theorem OAI.TwoPointCorrelations.mrt_exp_cos_inequality line 26
Source documentation
Corrected MRT Lemma A.8, proved using the monotonicity of exp x - x² rather than a second derivative at a square root.
```
theorem mrt_exp_cos_inequality (a θ : ℝ) :
    Real.exp a + Real.exp (-a) - 2 * Real.cos θ ≤
      Real.exp (Real.sqrt (a ^ 2 + θ ^ 2)) := by
…
```
lemma OAI.TwoPointCorrelations.mrt_exp_difference_square line 49
theorem OAI.TwoPointCorrelations.mrt_exp_difference_bound line 74
theorem OAI.TwoPointCorrelations.mrt_normalized_band_bound line 86

theorem OAI.TwoPointCorrelations.mrt_normalized_bands_bound line 96

Source documentation

Every band contributes at most one after normalization. In particular this product incurs no loss depending on the number of bands.

theorem mrt_normalized_bands_bound {ι : Type*} (J : Finset ι)
    (z : ι → ℂ) (M : ι → ℝ) (hM : ∀ j ∈ J, ‖z j‖ ≤ M j) :
    (∏ j ∈ J, ‖Complex.exp (z j / 2) - Complex.exp (-z j / 2)‖ *
      Real.exp (-M j / 2)) ≤ 1 := by
…