OAI/Analysis/BernoulliCone/IntegratedPrimitive.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.DeSilvaJerison.shiftU line 12
2. def OAI.Bernoulli.DeSilvaJerison.ceilingGraph line 13
3. def OAI.Bernoulli.DeSilvaJerison.comparisonR line 14
4. lemma OAI.Bernoulli.DeSilvaJerison.shiftU_lipschitz line 18
5. lemma OAI.Bernoulli.DeSilvaJerison.ceilingGraph_lipschitz line 23
6. lemma OAI.Bernoulli.DeSilvaJerison.ceiling_eq_shift_outside line 26
7. lemma OAI.Bernoulli.DeSilvaJerison.ceiling_sub_compact line 30
8. lemma OAI.Bernoulli.DeSilvaJerison.comparison_primitive_support line 36
9. lemma OAI.Bernoulli.DeSilvaJerison.comparison_primitive_compact line 43
10. lemma OAI.Bernoulli.DeSilvaJerison.shiftU_gradient line 48
11. lemma OAI.Bernoulli.DeSilvaJerison.ceilingGraph_gradient line 53
12. lemma OAI.Bernoulli.DeSilvaJerison.comparisonR_ae_bound line 62
13. lemma OAI.Bernoulli.DeSilvaJerison.comparisonR_measurable line 84
14. lemma OAI.Bernoulli.DeSilvaJerison.comparisonR_bound line 92
15. theorem OAI.Bernoulli.DeSilvaJerison.comparisonR_integral_nonneg line 111

    Source documentation

    The genuine compact graph primitive yields an integrated comparison at positive height. Hypotheses concern a competitor, never desired minimality.

    theorem comparisonR_integral_nonneg {v:Space 7→ℝ} {L:ℝ≥0} (hv:LipschitzWith L v)
        {ε:ℝ} (hε:0<ε) (hc:HasCompactSupport (fun y=>v y-U y))
        {c:Space 7} {r:ℝ} (hS:tsupport (fun y=>v y-U y)⊆Metric.ball c r) :
        0≤∫x in Metric.ball c r,comparisonR ε v x := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.comparisonR