OAI/Analysis/DiskMaximal/AbsoluteContinuity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SobolevBand.high_dyadic line 57
2. lemma OAI.SobolevBand.small_dyadic line 62
3. lemma OAI.SobolevBand.small_le_high line 67
4. lemma OAI.SobolevBand.gradient_error_restrict line 73
5. lemma OAI.SobolevBand.exists_diagonal_smooth line 83
6. lemma OAI.SobolevBand.smooth_diagonal_local_L1 line 112
7. lemma OAI.WeakCompact.densityLimit_compact_bound_limit line 147
8. lemma OAI.NullLocalization.thickening_null_integral line 166
9. lemma OAI.NullLocalization.local_split_bound line 187
10. lemma OAI.NullLocalization.diagonal_density_limit_ac line 214
11. lemma OAI.WeakCompact.densityLimit_rn line 271
12. lemma OAI.WeakSobolev.local_L1_test_converges line 292
13. lemma OAI.SobolevBand.positive_direction_limit line 323

    Source documentation

    Positive directional densities share a single ultrafilter, so their differences retain the distributional identities. Absolute continuity is proved by local small-radius cutoff estimates, rather than assumed as a BV compactness upgrade.

    lemma positive_direction_limit : ∃ C : ℝ, 0<C ∧
        ∀ {u : ℕ → ℂ → ℝ} {g : ℂ → ℂ},
        (∀ n, ContDiff ℝ 1 (u n) ∧ HasCompactSupport (u n)) → Integrable g →
        (∀ n, (∫ x,‖gradient (u n) x‖)≤(∫ x,‖g x‖)+1) →
        Tendsto (fun n => ∫ x,‖gradient (u n) x-g x‖) atTop (𝓝 0) →
        ∀ v : ℂ, ‖v‖≤1 → ∃ d : ℂ → ℝ, Integrable d ∧ (∀ x,0≤d x) ∧
          (∫ x,d x)≤2*C*(∫ x,‖g x‖) ∧
          ∀ φ : C_c(ℂ,ℝ), Tendsto
            (fun n => ∫ x,(‖gradient (band (u n) (low n) (high n)) x‖+
              ⟪gradient (band (u n) (low n) (high n)) x,v⟫)*φ x)
            (hyperfilter ℕ) (𝓝 (∫ x,d x*φ x)) := by
    …

    Mentions: OAI.SobolevBand.band, OAI.SobolevBand.low, OAI.SobolevBand.high

14. lemma OAI.WeakSobolev.direction_identity_limit line 373
15. lemma OAI.WeakSobolev.complex_inner_one line 413
16. lemma OAI.WeakSobolev.complex_inner_I line 415
17. lemma OAI.WeakSobolev.complex_hasGradient_of_coordinates line 418
18. lemma OAI.SobolevBand.complex_endpoint line 453

    Source documentation

    The all-radius absolute endpoint on the isometric complex model of the plane. No smoothness, sign, compact support, or boundedness remains on the input.

    lemma complex_endpoint : ∃ C : ℝ, 0<C ∧ ∀ (f : ℂ → ℝ) (g : ℂ → ℂ),
        Integrable f → Integrable g → HasGradient (μ := volume) f g →
    …

19. lemma OAI.WeakSobolev.HasGradient.comp_isometry line 507