OAI/Analysis/CoulombTransport/Calibration.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem356.shiftedPotential line 13

   Source documentation

   A bounded-below signed potential is made nonnegative by a constant shift.

   def shiftedPotential (u : E3 → ℝ) (M : ℝ) (x : E3) : ℝ≥0∞ :=
   …

   Mentions: OAI.Problem356.E3

2. lemma OAI.Problem356.measurable_shiftedPotential line 16
3. lemma OAI.Problem356.shifted_three_sum line 20
4. lemma OAI.Problem356.shifted_three_le line 31
5. lemma OAI.Problem356.shifted_three_eq_of_contact line 39
6. lemma OAI.Problem356.contact_of_shifted_three_eq line 46
7. lemma OAI.Problem356.shifted_three_eq_iff line 66
8. lemma OAI.Problem356.shifted_three_le_iff line 75

   Source documentation

   The shift preserves the supporting inequality, including negative signed sums.

   lemma shifted_three_le_iff {a b c M : ℝ} {z : ℝ≥0∞}
       (ha : -M ≤ a) (hb : -M ≤ b) (hc : -M ≤ c) (hM : 0 ≤ M) :
       (ENNReal.ofReal (a + M) + ENNReal.ofReal (b + M) + ENNReal.ofReal (c + M) ≤
         z + ENNReal.ofReal (3 * M)) ↔ ENNReal.ofReal (a + b + c) ≤ z := by
   …

9. lemma OAI.Problem356.shifted_three_eq_iff_of_pos line 89

   Source documentation

   For a positive cost, equality already forces nonnegativity of the signed sum.

   lemma shifted_three_eq_iff_of_pos {a b c M : ℝ} {z : ℝ≥0∞}
       (ha : -M ≤ a) (hb : -M ≤ b) (hc : -M ≤ c) (hM : 0 ≤ M)
       (hz : 0 < z) :
       (ENNReal.ofReal (a + M) + ENNReal.ofReal (b + M) + ENNReal.ofReal (c + M) =
         z + ENNReal.ofReal (3 * M)) ↔ ENNReal.ofReal (a + b + c) = z := by
   …

10. lemma OAI.Problem356.shiftedPotential_certificate line 102
11. lemma OAI.Problem356.shiftedPotential_contact_iff line 111
12. lemma OAI.Problem356.lintegral_shiftedPotential_le_of_ae_le line 123

    Source documentation

    An almost-everywhere upper bound suffices for finiteness of the shifted potential; no signed-integrability conversion is needed.

    lemma lintegral_shiftedPotential_le_of_ae_le {mu : Measure E3} [IsProbabilityMeasure mu]
        {u : E3 → ℝ} {M A : ℝ} (hbound : ∀ᵐ x ∂mu, u x ≤ A) :
        (∫⁻ x, shiftedPotential u M x ∂mu) ≤ ENNReal.ofReal (A + M) := by
    …

    Mentions: OAI.Problem356.E3, OAI.Problem356.shiftedPotential

13. lemma OAI.Problem356.lintegral_shiftedPotential_lt_top_of_ae_le line 132
14. lemma OAI.Problem356.lintegral_shiftedPotential line 138
15. lemma OAI.Problem356.lintegral_shiftedPotential_lt_top line 155