OAI/Analysis/BernoulliCone/ThresholdRecovery.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.ThresholdRecovery.integral_norm_sq_eq line 17
2. lemma OAI.Bernoulli.ThresholdRecovery.tendsto_integral_norm_sq line 24
3. def OAI.Bernoulli.ThresholdRecovery.ramp line 37
4. lemma OAI.Bernoulli.ThresholdRecovery.ramp_continuous line 38
5. lemma OAI.Bernoulli.ThresholdRecovery.ramp_nonneg line 41
6. lemma OAI.Bernoulli.ThresholdRecovery.ramp_le_one line 42
7. lemma OAI.Bernoulli.ThresholdRecovery.ramp_norm_le line 43
8. def OAI.Bernoulli.ThresholdRecovery.envelope line 46
9. lemma OAI.Bernoulli.ThresholdRecovery.envelope_norm_le line 47
10. lemma OAI.Bernoulli.ThresholdRecovery.phase_threshold_le line 52
11. lemma OAI.Bernoulli.ThresholdRecovery.envelope_le_phase line 67
12. lemma OAI.Bernoulli.ThresholdRecovery.envelope_measurable line 79
13. lemma OAI.Bernoulli.ThresholdRecovery.envelope_integrable line 86
14. lemma OAI.Bernoulli.ThresholdRecovery.envelope_integral_tendsto line 91
15. lemma OAI.Bernoulli.ThresholdRecovery.h1_const_ball line 108
16. lemma OAI.Bernoulli.ThresholdRecovery.h1_sub_const_ball line 111
17. lemma OAI.Bernoulli.ThresholdRecovery.fixed_threshold_limit line 118

    Source documentation

    Strong H1-density gives the exact upper comparison after fixed positive threshold truncation. The discontinuous phase term is controlled by a continuous ramp, not by an unjustified continuity assertion for positivity sets.

    lemma fixed_threshold_limit {c:Space d} {r:ℝ} {u w:Space d→ℝ}
        {G W:Space d→Space d} (hu:H1 (Metric.ball c r) u G)
        (hw:H10 (Metric.ball c r) w W)
        (hun:∀ᵐ x ∂volume.restrict (Metric.ball c r),0≤u x)
        (hwn:∀ᵐ x ∂volume.restrict (Metric.ball c r),0≤w x)
        {ε:ℝ} (hε:0<ε)
        (hcomp:∀φ:Space d→ℝ,Test (Metric.ball c r) φ →
          energy (Metric.ball c r) u G≤energy (Metric.ball c r)
            (fun x=>u x+max (φ x-ε) 0)
            (fun x=>G x+(if 0<φ x-ε then (1:ℝ) else 0) • gradient φ x)) :
        energy (Metric.ball c r) u G≤
          (∫x in Metric.ball c r,‖G x+(if 0<w x-ε then (1:ℝ) else 0) • W x‖^2)+
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.H10, OAI.Bernoulli.Test, OAI.Bernoulli.energy

18. theorem OAI.Bernoulli.ThresholdRecovery.upper_variation_of_threshold_tests line 180

    Source documentation

    The faithful arbitrary-Sobolev upper-variation bridge. The sole comparison input here is the concrete thresholded compact-test inequality; all density and phase-limit steps are proved, without regularity assumptions on the competitor.

    theorem upper_variation_of_threshold_tests {c:Space d} {r:ℝ} {u w:Space d→ℝ}
        {G W:Space d→Space d} (hu:H1 (Metric.ball c r) u G)
        (hw:H10 (Metric.ball c r) w W)
        (hun:∀ᵐ x ∂volume.restrict (Metric.ball c r),0≤u x)
        (hwn:∀ᵐ x ∂volume.restrict (Metric.ball c r),0≤w x)
        (hcomp:∀ε:ℝ,0<ε → ∀φ:Space d→ℝ,Test (Metric.ball c r) φ →
          energy (Metric.ball c r) u G≤energy (Metric.ball c r)
            (fun x=>u x+max (φ x-ε) 0)
            (fun x=>G x+(if 0<φ x-ε then (1:ℝ) else 0) • gradient φ x)) :
        energy (Metric.ball c r) u G≤energy (Metric.ball c r)
          (fun x=>u x+w x) (fun x=>G x+W x) := by
    …

    Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.H10, OAI.Bernoulli.Test, OAI.Bernoulli.energy