OAI/Geometry/RCD/Heat/HeatToleranceSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing splitting smallness before the geometric neighborhood

  1. theorem OAI.RegularPointCoordinates.exists_cumulative_error_tolerance line 12

    Source documentation

    A single positive tolerance enforces the mean-comparison and cumulative absorption thresholds. All constants are fixed before the map and radius.

    theorem exists_cumulative_error_tolerance {a C W M cap : ℝ}
    (ha : 0 ≤ a) (hC : 0 ≤ C) (hW : 0 ≤ W) (hM : 0 ≤ M) (hcap : 0 < cap) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ cap ∧ ε ≤ 1 ∧ ∀ e : ℝ, 0 ≤ e → e ≤ ε →
      a * e ≤ 1 / 64 ∧ 2 * C * W * (M * e) ≤ 1 / 2 := by
…