CoareaInput.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Scalar coarea and its finite-energy consequences

The planar scalar coarea identities specialize Federer, Geometric Measure Theory, Springer (1969), §3.2.11 (coarea) and §3.2.12 (weighted coarea), DOI: 10.1007/978-3-642-62010-2. For a C¹ real function on an open subset of the Euclidean plane, the integral of the one-dimensional Hausdorff measures of its fibers equals the integral of the norm of its differential. The locally Lipschitz version follows from the stated Lipschitz coarea theorem by a countable relatively compact covering.

PlanarScalarCoarea and WeightedPlanarScalarCoarea express these specializations as propositions. They require neither finite energy nor topological conclusions. The length function need only be Lebesgue measurable; Borel measurability is unnecessary.

Finite area and finite squared differential imply finite integrated length, and integer periodization gives finite physical length for almost every circle-valued level.

def OAI.CircleDomainRigidity.scalarLevelLength line 36
def OAI.CircleDomainRigidity.ScalarCoareaIdentity line 41
Source documentation
Precisely the scalar planar coarea identity, including its required Lebesgue measurability assertion.
```
def ScalarCoareaIdentity (D : Set ℂ) (f : ℂ → ℝ) : Prop :=
…
```
def OAI.CircleDomainRigidity.PlanarScalarCoarea line 48
Source documentation
Federer (1969), §3.2.11, specialized to a real C¹ function on an open subset of the Euclidean plane.
```
def PlanarScalarCoarea : Prop :=
…
```
def OAI.CircleDomainRigidity.weightedScalarLevelLength line 52
def OAI.CircleDomainRigidity.weightedCircleLevelLength line 56
def OAI.CircleDomainRigidity.WeightedScalarCoareaIdentity line 62
Source documentation
Precisely the nonnegative weighted scalar coarea formula.
```
def WeightedScalarCoareaIdentity (D : Set ℂ) (f : ℂ → ℝ)
    (q : ℂ → ℝ≥0∞) : Prop :=
…
```
def OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea line 72
Source documentation
Federer (1969), §3.2.12, the nonnegative weighted coarea formula specialized to a scalar C¹ function on a planar open set. This is the identity used by eq:weighted-level-bound in §1 of the Koebe manuscript.
```
def WeightedPlanarScalarCoarea : Prop :=
…
```
theorem OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea.unweighted line 76
theorem OAI.CircleDomainRigidity.measurableSet_scalar_level line 90
Source documentation
The scalar fibers are measurable even though the function is only assumed continuous on its open domain.
```
theorem measurableSet_scalar_level {D : Set ℂ} (hD : IsOpen D)
    {f : ℂ → ℝ} (hf : ContinuousOn f D) (t : ℝ) :
    MeasurableSet (D ∩ {z | f z = t}) := by
…
```
theorem OAI.CircleDomainRigidity.weightedCircleLevelLength_eq_periodized line 105
Source documentation
Countable additivity on the disjoint integer lifts is the exact weighted circle-fiber identity.
```
theorem weightedCircleLevelLength_eq_periodized {D : Set ℂ} (hD : IsOpen D)
    {f : ℂ → ℝ} (hf : ContinuousOn f D) (q : ℂ → ℝ≥0∞) (t : ℝ) :
    weightedCircleLevelLength D f q t =
      periodizedLevelLength (weightedScalarLevelLength D f q) t := by
…
```
Mentions: OAI.CircleDomainRigidity.weightedCircleLevelLength, OAI.CircleDomainRigidity.periodizedLevelLength, OAI.CircleDomainRigidity.weightedScalarLevelLength
theorem OAI.CircleDomainRigidity.lintegral_periodizedLevelLength_of_aemeasurable line 120

theorem OAI.CircleDomainRigidity.weighted_circle_coarea line 135

Source documentation

The weighted circle-valued coarea formula follows from the real one, including the measurability needed for further integration.

theorem weighted_circle_coarea {D : Set ℂ} (hD : IsOpen D)
    {f : ℂ → ℝ} (hf : ContinuousOn f D) (q : ℂ → ℝ≥0∞)
    (hcoarea : WeightedScalarCoareaIdentity D f q) :
    AEMeasurable (weightedCircleLevelLength D f q)
        (volume.restrict (Ico (0 : ℝ) 1)) ∧
      (∫⁻ t in Ico (0 : ℝ) 1, weightedCircleLevelLength D f q t) =
        ∫⁻ z in D, q z * ENNReal.ofReal ‖fderiv ℝ f z‖ := by
…

Mentions: OAI.CircleDomainRigidity.WeightedScalarCoareaIdentity, OAI.CircleDomainRigidity.weightedCircleLevelLength

theorem OAI.CircleDomainRigidity.lintegral_differentialNorm_le_area_add_energy line 153

Source documentation

The elementary finite-measure L² → L¹ bound needed for coarea.

theorem lintegral_differentialNorm_le_area_add_energy (D : Set ℂ) (f : ℂ → ℝ) :
    (∫⁻ z in D, ENNReal.ofReal ‖fderiv ℝ f z‖) ≤
      volume D + ∫⁻ z in D, ENNReal.ofReal (‖fderiv ℝ f z‖ ^ 2) := by
…

theorem OAI.CircleDomainRigidity.scalar_coarea_integral_lt_top line 171

theorem OAI.CircleDomainRigidity.lintegral_weight_mul_differentialNorm_le_energies line 182

Source documentation

Square-integrability of the weight and differential controls their product. Only finiteness is needed here, so the elementary quadratic bound suffices.

theorem lintegral_weight_mul_differentialNorm_le_energies
    (D : Set ℂ) (f q : ℂ → ℝ) (hq : Measurable q) (hq0 : ∀ z, 0 ≤ q z) :
    (∫⁻ z in D, ENNReal.ofReal (q z) * ENNReal.ofReal ‖fderiv ℝ f z‖) ≤
      (∫⁻ z in D, ENNReal.ofReal (q z ^ 2)) +
        ∫⁻ z in D, ENNReal.ofReal (‖fderiv ℝ f z‖ ^ 2) := by
…

theorem OAI.CircleDomainRigidity.weighted_circle_coarea_of_finite_energy line 203

Source documentation

The weighted scalar coarea input gives the actual weighted circle formula and almost-everywhere finite weighted length under the paper's two L² assumptions.

theorem weighted_circle_coarea_of_finite_energy
    (hcoarea : WeightedPlanarScalarCoarea) {D : Set ℂ} (hD : IsOpen D)
    {f q : ℂ → ℝ} (hf : ContDiffOn ℝ 1 f D)
    (hq : Measurable q) (hq0 : ∀ z, 0 ≤ q z)
    (hq2 : (∫⁻ z in D, ENNReal.ofReal (q z ^ 2)) < ∞)
    (hf2 : (∫⁻ z in D, ENNReal.ofReal (‖fderiv ℝ f z‖ ^ 2)) < ∞) :
    AEMeasurable (weightedCircleLevelLength D f (fun z => ENNReal.ofReal (q z)))
        (volume.restrict (Ico (0 : ℝ) 1)) ∧
      (∫⁻ t in Ico (0 : ℝ) 1,
        weightedCircleLevelLength D f (fun z => ENNReal.ofReal (q z)) t) =
        (∫⁻ z in D, ENNReal.ofReal (q z) * ENNReal.ofReal ‖fderiv ℝ f z‖) ∧
      (∫⁻ t in Ico (0 : ℝ) 1,
…

Mentions: OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea, OAI.CircleDomainRigidity.weightedCircleLevelLength

theorem OAI.CircleDomainRigidity.ae_finite_hausdorffMeasure_scalar_mod_one_levels_of_aemeasurable line 230

Source documentation

Periodization remains valid for Lebesgue measurable lengths. The exceptional set and each of its integer translates are discarded before summing the real-level lengths.

theorem ae_finite_hausdorffMeasure_scalar_mod_one_levels_of_aemeasurable
    {Z : Type*} [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z]
    (f : Z → ℝ) (D : Set Z) (L : ℝ → ℝ≥0∞) (hL : AEMeasurable L volume)
    (hfinite : (∫⁻ t, L t) < ∞)
    (hlength : ∀ t, (μH[1] : Measure Z) (D ∩ {z | f z = t}) ≤ L t) :
    ∀ᵐ (t : ℝ) ∂volume.restrict (Ico (0 : ℝ) 1),
      (μH[1] : Measure Z) (D ∩ {z | (f z : UnitAddCircle) = (t : UnitAddCircle)}) < ∞ := by
…

theorem OAI.CircleDomainRigidity.ae_finite_planar_mod_one_levels line 254

Source documentation

The finite physical length conclusion from the coarea identity, finite area, and actual squared differential energy.

theorem ae_finite_planar_mod_one_levels {D : Set ℂ} {f : ℂ → ℝ}
    (hcoarea : ScalarCoareaIdentity D f) (harea : volume D < ∞)
    (henergy : (∫⁻ z in D, ENNReal.ofReal (‖fderiv ℝ f z‖ ^ 2)) < ∞) :
    ∀ᵐ (t : ℝ) ∂volume.restrict (Ico (0 : ℝ) 1),
      (μH[1] : Measure ℂ) (D ∩ {z | (f z : UnitAddCircle) = (t : UnitAddCircle)}) < ∞ :=
…

Mentions: OAI.CircleDomainRigidity.ScalarCoareaIdentity