LeafModulusRanges.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The leaf modulus from the giant, protected and compensation ranges

theorem OAI.Ostmann.leaf_modulus_lower_from_ranges line 11

Source documentation

P, U, and D are the products of protected, compensation, and outside spectator slots. The center identity is equation (45).

theorem leaf_modulus_lower_from_ranges
    (X x₁ x₂ P U D G tD J W Δ cG cP cU cD : ℝ)
    (hX : 0 < X) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hP : 0 < P) (hU : 0 < U) (hD : 0 < D)
    (hcenter : 2 * G + 2 * tD + J + W = Real.log X + Δ)
    (hg₁ : G - cG ≤ Real.log x₁) (hg₂ : G - cG ≤ Real.log x₂)
    (hp : J - cP ≤ Real.log P) (hu : W - cU ≤ Real.log U)
    (hd : 2 * tD - cD ≤ Real.log D) :
    X * Real.exp (Δ - (2 * cG + cP + cU + cD)) ≤ x₁ * x₂ * P * U * D := by
…

theorem OAI.Ostmann.leaf_sqrt_ratio_from_ranges line 37

Source documentation

The corresponding size of the square-root prefactor in a leaf of equation (50); the error in the exponent is independent of frequency.

theorem leaf_sqrt_ratio_from_ranges
    (X x₁ x₂ P U D G tD J W Δ cG cP cU cD : ℝ)
    (hX : 0 < X) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hP : 0 < P) (hU : 0 < U) (hD : 0 < D)
    (hcenter : 2 * G + 2 * tD + J + W = Real.log X + Δ)
    (hg₁ : G - cG ≤ Real.log x₁) (hg₂ : G - cG ≤ Real.log x₂)
    (hp : J - cP ≤ Real.log P) (hu : W - cU ≤ Real.log U)
    (hd : 2 * tD - cD ≤ Real.log D) :
    Real.sqrt (X / (x₁ * x₂ * P * U * D)) ≤
      Real.exp (((2 * cG + cP + cU + cD) - Δ) / 2) :=
…