WeightedPhysicalChart.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Weighted local chart estimates for actual quotient paths. The inverse chart distortion is kept explicit; the length is the existing physical occupation, with its original parameter multiplicity.

theorem OAI.CircleDomainRigidity.physical_chart_length_measure_le line 23
theorem OAI.CircleDomainRigidity.physical_chart_lintegral_le line 66
theorem OAI.CircleDomainRigidity.smooth_physical_chart_image_le line 80

theorem OAI.CircleDomainRigidity.quotient_smooth_image_le_physical line 107

Source documentation

The same weighted estimate for the actual quotient-coordinate image.

theorem quotient_smooth_image_le_physical (e : G ≃ₜ U) (hU : IsOpen U) (y₀ : Y)
    (π : Y → X) (hπ : Continuous π) (he : ∀ y : G, (e y).val = π y.val)
    (φ : ℂ → Y) (hφ : Continuous φ) {A D : Set ℂ} (hA : MeasurableSet A)
    (hφA : MeasurableSet (φ '' A)) (hAG : MapsTo φ A G) (hAD : A ⊆ D) (hD : IsOpen D)
    (j : Y → ℂ) (hjm : Measurable j) (hj : ∀ z ∈ A, j (φ z) = z)
    (B : ℝ≥0) (hB : LipschitzOnWith B j (φ '' A))
    (γ : FinitePhysicalPath e y₀) {f : ℂ → ℝ} (hf : ContDiffOn ℝ 1 f D)
    (F : X → ℝ) (Q : Set X) (hF : ∀ z ∈ A, F (π (φ z)) = f z)
    (hcover : ∀ x ∈ range γ.val ∩ Q, ∃ z ∈ A, π (φ z) = x) :
    volume (F '' (range γ.val ∩ Q)) ≤
      (B : ℝ≥0∞) * ∫⁻ y in φ '' A, ENNReal.ofReal ‖fderiv ℝ f (j y)‖
        ∂dyadicPhysicalOccupation e y₀ γ := by
…

Mentions: OAI.CircleDomainRigidity.FinitePhysicalPath, OAI.CircleDomainRigidity.dyadicPhysicalOccupation

theorem OAI.CircleDomainRigidity.smooth_physical_chart_circle_count_le line 125
theorem OAI.CircleDomainRigidity.quotient_smooth_interval_image_le_physical line 168