DyadicScalarBackground.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Absorbing scalar remainders into the actual dyadic mass envelope

theorem OAI.RegularPointCoordinates.dyadic_half_background_le line 17
Source documentation
The geometric background retains every error decaying at least like 2⁻ⁱ.
```
theorem dyadic_half_background_le (M : PositiveBilinearMeasure X E) (n : ℕ)
    (x : X) {R : ℝ} (hR : 0 ≤ R) (i : ℕ) (v : E) :
    (1 / 2 : ℝ) ^ i * ‖v‖ ^ 2 ≤ ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicBochnerEnvelope

theorem OAI.RegularPointCoordinates.dyadic_scalar_background_bounds line 31

Source documentation

All polynomial scalar terms needed in the source comparison are controlled by the same geometric background.

theorem dyadic_scalar_background_bounds (M : PositiveBilinearMeasure X E) (n : ℕ)
    (x : X) {R : ℝ} (hR : 0 < R) (hR1 : R ≤ 1) (i : ℕ) (v : E) :
    ((R / (2 : ℝ) ^ i) / R) * ‖v‖ ^ 2 ≤ ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ ∧
    (R / (2 : ℝ) ^ i) ^ 2 * ‖v‖ ^ 2 ≤ R ^ 2 * ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ ∧
    ((R / (2 : ℝ) ^ i) ^ 2 + (R / (2 : ℝ) ^ i) * R) * ‖v‖ ^ 2 ≤
      2 * R ^ 2 * ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ ∧
    ((R / (2 : ℝ) ^ i) ^ 2 + (R / (2 : ℝ) ^ i) * R ^ 2) * ‖v‖ ^ 2 ≤
      2 * R ^ 2 * ⟪v, dyadicBochnerEnvelope M n x R i v⟫_ℝ := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicBochnerEnvelope