ScaledMassBackground.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform coarse-mass background from a local scaled mass bound

theorem OAI.RegularPointCoordinates.dyadicBochnerMass_le_scaled_local line 18

Source documentation

Coarse masses use only the local measure, not arbitrary mass outside its Bochner equation region. The physical scale cancels exactly.

theorem dyadicBochnerMass_le_scaled_local (M : PositiveBilinearMeasure X E)
    (n : ℕ) {p x : X} {R D : ℝ} (hR : 0 < R) (hx : x ∈ ball p R)
    (hlocal : ∀ v, ⟪v, M.massOperator (ball p (2 * R)) v⟫_ℝ ≤
      D * (R ^ n / R ^ 2) * ‖v‖ ^ 2) (i : ℕ) (v : E) :
    ⟪v, dyadicBochnerMass M n x R i v⟫_ℝ ≤
      (((2 : ℝ) ^ i) ^ n / ((2 : ℝ) ^ i) ^ 2 * D) * ‖v‖ ^ 2 := by
…

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

theorem OAI.RegularPointCoordinates.exists_scaled_mass_background line 48

Source documentation

The finite omitted prefix is bounded before selecting the radius or the actual harmonic measure, once its local scaled mass is bounded.

theorem exists_scaled_mass_background (n J : ℕ) {D : ℝ} (hD : 0 ≤ D) :
    ∃ b : ℝ, 1 ≤ b ∧ ∀ (R : ℝ), 0 < R → ∀ (p : X) (M : PositiveBilinearMeasure X E),
      (∀ v, ⟪v, M.massOperator (ball p (2 * R)) v⟫_ℝ ≤
        D * (R ^ n / R ^ 2) * ‖v‖ ^ 2) →
      ∀ x ∈ ball p R, ∀ 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