OAI/Geometry/PlaneColoring/Expansion.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.positive_log_difference_bound line 9
  2. lemma OAI.EuclideanFiveColor.controlled_interval_derivative line 26
  3. lemma OAI.EuclideanFiveColor.controlled_interval_expands line 36
  4. lemma OAI.EuclideanFiveColor.geometric_partial_sum line 46
  5. def OAI.EuclideanFiveColor.iterComposition line 63
  6. def OAI.EuclideanFiveColor.iterDerivative line 66
  7. lemma OAI.EuclideanFiveColor.iterComposition_hasDeriv line 70
  8. lemma OAI.EuclideanFiveColor.iterDerivative_pos line 75
  9. lemma OAI.EuclideanFiveColor.iterComposition_strictMono line 80
  10. lemma OAI.EuclideanFiveColor.iterDerivative_log_oscillation line 86
  11. lemma OAI.EuclideanFiveColor.iterDerivative_ratio_bound line 124
  12. lemma OAI.EuclideanFiveColor.eventually_reaches_threshold line 140
  13. lemma OAI.EuclideanFiveColor.first_expansion_threshold line 164
  14. lemma OAI.EuclideanFiveColor.exists_expanding_word line 201
  15. lemma OAI.EuclideanFiveColor.line_lipschitzOn_image_bound line 259
  16. lemma OAI.EuclideanFiveColor.interval_defect_image_bound line 263
  17. lemma OAI.EuclideanFiveColor.derivative_ratio_lipschitzOn line 286
  18. lemma OAI.EuclideanFiveColor.line_volume_preimage_bound line 307
  19. lemma OAI.EuclideanFiveColor.line_map_restrict_volume_le line 321
  20. lemma OAI.EuclideanFiveColor.integrable_comp_of_map_le line 344
  21. lemma OAI.EuclideanFiveColor.integral_norm_comp_le line 350
  22. lemma OAI.EuclideanFiveColor.tendsto_integral_norm_comp_sub line 360

    Source documentation

    L¹ continuity under measurable perturbations with a common bounded pushforward density.

    lemma tendsto_integral_norm_comp_sub [IsFiniteMeasure μ] [ν.WeaklyRegular]
    {T : ℕ → X → Y} {S : X → Y} {C : ℝ≥0}
    (hT : ∀ n, Measurable (T n)) (hS : Measurable S)
    (hmT : ∀ n, μ.map (T n) ≤ (C : ENNReal) • ν) (hmS : μ.map S ≤ (C : ENNReal) • ν)
    (ht : ∀ᵐ x ∂μ, Tendsto (fun n => T n x) atTop (𝓝 (S x)))
    {f : Y → ℝ} (hf : Integrable f ν) :
    Tendsto (fun n => ∫ x, ‖f (T n x)-f (S x)‖ ∂μ) atTop (𝓝 0) := by
…
  23. lemma OAI.EuclideanFiveColor.tendsto_integral_norm_comp_sub_eventual line 420
  24. lemma OAI.EuclideanFiveColor.line_antilipschitz_qmp line 442
  25. lemma OAI.EuclideanFiveColor.line_indicator_pullback_L1 line 449
  26. lemma OAI.EuclideanFiveColor.deriv_lower_antilipschitz line 473
  27. lemma OAI.EuclideanFiveColor.deriv_lower_qmp line 486
  28. lemma OAI.EuclideanFiveColor.iterComposition_invariant line 492
  29. lemma OAI.EuclideanFiveColor.expanding_interval_defect line 506
  30. lemma OAI.EuclideanFiveColor.periodic_interval_defect line 546
  31. lemma OAI.EuclideanFiveColor.periodic_interval_normalize line 555
  32. lemma OAI.EuclideanFiveColor.compact_almost_conull_interval line 567
  33. lemma OAI.EuclideanFiveColor.exists_density_interval line 592
  34. lemma OAI.EuclideanFiveColor.expansion_almost_conull line 621
  35. lemma OAI.EuclideanFiveColor.expansion_conull_interval line 642
  36. lemma OAI.EuclideanFiveColor.conull_extend_intervals line 673
  37. lemma OAI.EuclideanFiveColor.conull_interval_alternation_false line 701