UniformMassBackground.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One finite coarse-scale mass bound for every center

theorem OAI.RegularPointCoordinates.dyadicBochnerMass_le_total line 18

Source documentation

The total full Bochner measure bounds the scaled mass at any center.

theorem dyadicBochnerMass_le_total (M : PositiveBilinearMeasure X E) (n : ℕ)
    {R : ℝ} (hR : 0 < R) (i : ℕ) (x : X) (v : E) :
    ⟪v, dyadicBochnerMass M n x R i v⟫_ℝ ≤
      ((R / 2 ^ i) ^ 2 / (R / 2 ^ i) ^ n) * ‖M.massOperator univ‖ * ‖v‖ ^ 2 := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.dyadicBochnerMass

theorem OAI.RegularPointCoordinates.exists_uniform_mass_background line 31

Source documentation

The finitely many omitted scales have a single finite background constant, independent of the ball center.

theorem exists_uniform_mass_background (M : PositiveBilinearMeasure X E)
    (n : ℕ) {R : ℝ} (hR : 0 < R) (J : ℕ) :
    ∃ b : ℝ, 1 ≤ b ∧ ∀ x i v,
      ⟪v, dyadicBochnerEnvelope M n x R (J + i) v⟫_ℝ ≤
        b * (3 / 4 : ℝ) ^ i * ‖v‖ ^ 2 +
          ∑ j ∈ Finset.range (i + 1), (3 / 4 : ℝ) ^ (i - j) *
            ⟪v, dyadicBochnerMass M n x R (J + j) v⟫_ℝ := by
…

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