ScaledStampacchia.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Scale-invariant extinction of superlevel distributions

theorem OAI.RegularPointCoordinates.rescaled_superlevel_coefficient line 12

Source documentation

The exact cancellation of height and volume factors in a superlevel recurrence. Keeping these factors is essential when the ball shrinks.

theorem rescaled_superlevel_coefficient {R A M H p y t : ℝ}
    (hM : 0 < M) (hH : 0 < H) (hy : 0 ≤ y) (ht : 0 < t)
    (hscale : R * M ^ (p - 2) = A * H ^ p) :
    (R * (M * y) ^ (p - 1) / (H * t) ^ p) / M =
      A * y ^ (p - 1) / t ^ p := by
…

theorem OAI.RegularPointCoordinates.exists_scaled_extinction_level line 29

Source documentation

A uniform extinction constant survives simultaneous rescaling of the height and the initial volume.

theorem exists_scaled_extinction_level {A p : ℝ} (hA : 0 ≤ A) (hp : 2 < p) :
    ∃ K : ℝ, 0 < K ∧ ∀ (R M H : ℝ), 0 < M → 0 < H →
      R * M ^ (p - 2) = A * H ^ p → ∀ Y : ℝ → ℝ,
      (∀ k, 0 ≤ k → 0 ≤ Y k) → Y 0 ≤ M →
      (∀ k l, 0 ≤ k → k ≤ l → Y l ≤ Y k) →
      (∀ k l, 0 ≤ k → k < l → Y l ≤ R * Y k ^ (p - 1) / (l - k) ^ p) →
      Y (K * H) = 0 := by
…

theorem OAI.RegularPointCoordinates.normalized_sobolev_coefficient line 64

Source documentation

The normalized Dirichlet Sobolev coefficient has precisely the homogeneity required by the superlevel recurrence.

theorem normalized_sobolev_coefficient {C s V d : ℝ}
    (hC : 0 ≤ C) (hs : 0 < s) (hV : 0 < V) (hd : 1 < d) :
    (C * s * V ^ (1 / d - 1)) ^ (2 * d) * V ^ (2 * d - 2) =
      C ^ (2 * d) * s ^ (2 * d) := by
…